Agda.Interaction.Highlighting.Precise
Description
Types used for precise syntax highlighting.
- data Aspect
- data NameKind
- data OtherAspect
- data MetaInfo = MetaInfo {
- aspect :: Maybe Aspect
- otherAspects :: [OtherAspect]
- note :: Maybe String
- definitionSite :: Maybe (TopLevelModuleName, Integer)
- data File
- type HighlightingInfo = CompressedFile
- singleton :: Range -> MetaInfo -> File
- several :: [Range] -> MetaInfo -> File
- smallestPos :: File -> Maybe Integer
- toMap :: File -> Map Integer MetaInfo
- type CompressedFile = [(Range, MetaInfo)]
- compress :: File -> CompressedFile
- decompress :: CompressedFile -> File
- tests :: IO Bool
Documentation
Various more or less syntactic aspects of the code. (These cannot overlap.)
data OtherAspect Source
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 |
Meta information which can be associated with a character/character range.
Constructors
| MetaInfo | |
Fields
| |
A File is a mapping from file positions to meta information.
The first position in the file has number 1.
type HighlightingInfo = CompressedFileSource
Syntax highlighting information for a given source file.
singleton :: Range -> MetaInfo -> FileSource
singleton r mr, and
in which every position is associated with m.
several :: [Range] -> MetaInfo -> FileSource
Like singleton, but with several ranges instead of only one.
toMap :: File -> Map Integer MetaInfoSource
Convert the File to a map from file positions (counting from 1)
to meta information.
type CompressedFile = [(Range, MetaInfo)]Source
compress :: File -> CompressedFileSource
Compresses a file by merging consecutive positions with equal meta information into longer ranges.
decompress :: CompressedFile -> FileSource
Decompresses a compressed file.