| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Highlighting.Precise
Description
Types used for precise syntax highlighting.
Synopsis
- data Aspect
- data NameKind
- data OtherAspect
- data Aspects = Aspects {}
- data DefinitionSite = DefinitionSite {}
- data TokenBased
- newtype RangePair = RangePair {}
- rangePairInvariant :: RangePair -> Bool
- newtype PositionMap = PositionMap {}
- newtype DelayedMerge hl = DelayedMerge (Endo [hl])
- delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool
- type HighlightingInfo = RangeMap Aspects
- highlightingInfoInvariant :: HighlightingInfo -> Bool
- type HighlightingInfoBuilder = DelayedMerge RangePair
- highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool
- parserBased :: Aspects
- kindOfNameToNameKind :: KindOfName -> NameKind
- class IsBasicRangeMap a m | m -> a where
- several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl
- class Convert a b where
- convert :: a -> b
- insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
- restrictTo :: Range -> RangeMap a -> RangeMap a
Highlighting information
Syntactic aspects of the code. (These cannot overlap.)
Constructors
| Comment | |
| Keyword | |
| String | |
| Number | |
| Hole | |
| Symbol | Symbols like forall, =, ->, etc. |
| PrimitiveType | Things like Set and Prop. |
| Name (Maybe NameKind) Bool | Is the name an operator part? |
| Pragma | Text occurring in pragmas that does not have a more specific aspect. |
| Background | Non-code contents in literate Agda |
| Markup | Delimiters used to separate the Agda code blocks from the other contents in literate Agda |
Instances
NameKinds are figured out during scope checking.
Constructors
| Bound | Bound variable. |
| Generalizable | Generalizable variable. (This includes generalizable variables that have been generalized). |
| Constructor Induction | Inductive or coinductive constructor. |
| Datatype | |
| Field | Record field. |
| Function | |
| Module | Module name. |
| Postulate | |
| Primitive | Primitive. |
| Record | Record type. |
| Argument | Named argument, like x in {x = v} |
| Macro | Macro. |
Instances
data OtherAspect Source #
Other aspects, generated by type checking.
(These can overlap with each other and with Aspects.)
Constructors
| Error | |
| ErrorWarning | A warning that is considered fatal in the end. |
| DottedPattern | |
| UnsolvedMeta | |
| UnsolvedConstraint | Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint. |
| TerminationProblem | |
| PositivityProblem | |
| Deadcode | Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc. |
| ShadowingInTelescope | Used for shadowed repeated variable names in telescopes. |
| CoverageProblem | |
| IncompletePattern | When this constructor is used it is probably a good idea to
include a |
| TypeChecks | Code which is being type-checked. |
| MissingDefinition | Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode. |
| CatchallClause | |
| ConfluenceProblem |
Instances
Meta information which can be associated with a character/character range.
Constructors
| Aspects | |
Fields
| |
Instances
data DefinitionSite Source #
Constructors
| DefinitionSite | |
Fields
| |
Instances
data TokenBased Source #
Is the highlighting "token-based", i.e. based only on information from the lexer?
Constructors
| TokenBased | |
| NotOnlyTokenBased |
Instances
A limited kind of syntax highlighting information: a pair
consisting of Ranges and Aspects.
Note the invariant which RangePairs should satisfy
(rangePairInvariant).
Instances
| Show RangePair Source # | |
| NFData RangePair Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| IsBasicRangeMap Aspects RangePair Source # | |
| IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Convert (DelayedMerge RangePair) PositionMap Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods | |
| Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
newtype PositionMap Source #
Syntax highlighting information, represented by maps from
positions to Aspects.
The first position in the file has number 1.
Constructors
| PositionMap | |
Fields | |
Instances
newtype DelayedMerge hl Source #
Highlighting info with delayed merging.
Merging large sets of highlighting info repeatedly might be costly. The idea of this type is to accumulate small pieces of highlighting information, and then to merge them all at the end.
Note the invariant which values of this type should satisfy
(delayedMergeInvariant).
Constructors
| DelayedMerge (Endo [hl]) |
Instances
delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool Source #
Invariant for DelayedMerge hlhl.
Additionally the endofunction should be extensionally equal to (fs
for some list ++)fs.
type HighlightingInfo = RangeMap Aspects Source #
Highlighting information.
Note the invariant which values of this type should satisfy
(highlightingInfoInvariant).
This is a type synonym in order to make it easy to change to another representation.
highlightingInfoInvariant :: HighlightingInfo -> Bool Source #
The invariant for HighlightingInfo.
type HighlightingInfoBuilder = DelayedMerge RangePair Source #
A type that is intended to be used when constructing highlighting information.
Note the invariant which values of this type should satisfy
(highlightingInfoBuilderInvariant).
This is a type synonym in order to make it easy to change to another representation.
The type should be an instance of IsBasicRangeMap AspectsSemigroup and Monoid, and there should be an instance of
Convert HighlightingInfoBuilder HighlightingInfo
highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool Source #
The invariant for HighlightingInfoBuilder.
Additionally the endofunction should be extensionally equal to (fs
for some list ++)fs.
Operations
parserBased :: Aspects Source #
A variant of mempty with tokenBased set to
NotOnlyTokenBased.
kindOfNameToNameKind :: KindOfName -> NameKind Source #
Conversion from classification of the scope checker.
class IsBasicRangeMap a m | m -> a where Source #
A class that is intended to make it easy to swap between different range map implementations.
Note that some RangeMap operations are not included in this
class.
Methods
singleton :: Ranges -> a -> m Source #
The map singleton rs xrs, and
every position in those ranges is associated with x.
toMap :: m -> IntMap a Source #
Converts range maps to IntMaps from positions to values.
toList :: m -> [(Range, a)] Source #
Converts the map to a list. The ranges are non-overlapping and non-empty, and earlier ranges precede later ones in the list.
coveringRange :: m -> Maybe Range Source #
Returns the smallest range covering everything in the map (or
Nothing, if the range would be empty).
Note that the default implementation of this operation might be inefficient.
Instances
class Convert a b where Source #
Conversion between different types.
Instances
| Convert PositionMap (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Monoid hl => Convert (DelayedMerge hl) hl Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source # | |
| Convert (DelayedMerge RangePair) PositionMap Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods | |
| Convert (RangeMap Aspects) (RangeMap Aspects) Source # | |
| Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source # | |
| Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |