|
Agda.Interaction.Highlighting.Precise |
|
|
Description |
Types used for precise syntax highlighting.
|
|
Synopsis |
|
|
|
Documentation |
|
|
Various more or less syntactic aspects of the code. (These cannot
overlap.)
| Constructors | Comment | | Keyword | | String | | Number | | Symbol | Symbols like forall, =, ->, etc.
| PrimitiveType | Things like Set and Prop.
| Name (Maybe NameKind) Bool | Is the name an operator part?
|
| Instances | |
|
|
|
Constructors | Bound | Bound variable.
| Constructor Induction | Inductive or coinductive constructor.
| Datatype | | Field | Record field.
| Function | | Module | Module name.
| Postulate | | Primitive | Primitive.
| Record | Record type.
|
| Instances | |
|
|
|
Other aspects. (These can overlap with each other and with
Aspects.)
| Constructors | Error | | DottedPattern | | UnsolvedMeta | | TerminationProblem | | IncompletePattern | When this constructor is used it is probably a good idea to
include a note explaining why the pattern is incomplete.
|
| Instances | |
|
|
|
Meta information which can be associated with a
character/character range.
| Constructors | MetaInfo | | aspect :: Maybe Aspect | | otherAspects :: [OtherAspect] | | note :: Maybe String | This note, if present, can be displayed as a tool-tip or
something like that. It should contain useful information about
the range (like the module containing a certain identifier, or
the fixity of an operator).
| definitionSite :: Maybe (TopLevelModuleName, Integer) | The definition site of the annotated thing, if applicable and
known. File positions are counted from 1.
|
|
| Instances | |
|
|
|
A File is a mapping from file positions to meta information.
The first position in the file has number 1.
| Instances | |
|
|
|
Syntax highlighting information for a given source file.
|
|
|
singleton r m is a file whose positions are those in r, and
in which every position is associated with m.
|
|
|
Like singleton, but with several ranges instead of only one.
|
|
|
Returns the smallest position, if any, in the File.
|
|
|
Convert the File to a map from file positions (counting from 1)
to meta information.
|
|
|
A compressed File, in which consecutive positions with the same
MetaInfo are stored together.
|
|
|
Compresses a file by merging consecutive positions with equal
meta information into longer ranges.
|
|
|
Decompresses a compressed file.
|
|
|
All the properties.
|
|
Produced by Haddock version 2.4.2 |