Safe Haskell | Safe-Infered |
---|
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
data Aspect
Various more or less syntactic aspects of the code. (These cannot overlap.)
data NameKind
data OtherAspect
Other aspects. (These can overlap with each other and with
Aspect
s.)
Constructors
Error | |
DottedPattern | |
UnsolvedMeta | |
TerminationProblem | |
IncompletePattern | When this constructor is used it is probably a good idea to
include a |
data MetaInfo
Meta information which can be associated with a character/character range.
Constructors
MetaInfo | |
Fields
|
data File
A File
is a mapping from file positions to meta information.
The first position in the file has number 1.
type HighlightingInfo = CompressedFile
Syntax highlighting information for a given source file.
singleton :: Range -> MetaInfo -> File
is a file whose positions are those in singleton
r mr
, and
in which every position is associated with m
.
smallestPos :: File -> Maybe Integer
Returns the smallest position, if any, in the File
.
toMap :: File -> Map Integer MetaInfo
Convert the File
to a map from file positions (counting from 1)
to meta information.
type CompressedFile = [(Range, MetaInfo)]
compress :: File -> CompressedFile
Compresses a file by merging consecutive positions with equal meta information into longer ranges.
decompress :: CompressedFile -> File
Decompresses a compressed file.