Safe Haskell | None |
---|---|
Language | Haskell98 |
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 :: Ranges -> MetaInfo -> File
- several :: [Ranges] -> MetaInfo -> File
- smallestPos :: File -> Maybe Integer
- toMap :: File -> Map Integer MetaInfo
- newtype CompressedFile = CompressedFile {}
- compressedFileInvariant :: CompressedFile -> Bool
- compress :: File -> CompressedFile
- decompress :: CompressedFile -> File
- noHighlightingInRange :: Ranges -> CompressedFile -> CompressedFile
- singletonC :: Ranges -> MetaInfo -> CompressedFile
- severalC :: [Ranges] -> MetaInfo -> CompressedFile
- splitAtC :: Integer -> CompressedFile -> (CompressedFile, CompressedFile)
- smallestPosC :: CompressedFile -> Maybe Integer
- tests :: IO Bool
Files
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 | |
UnsolvedConstraint | Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint. |
TerminationProblem | |
IncompletePattern | When this constructor is used it is probably a good idea to
include a |
TypeChecks | Code which is being type-checked. |
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.
Creation
singleton :: Ranges -> MetaInfo -> File
is a file whose positions are those in singleton
rs mrs
,
and in which every position is associated with m
.
Inspection
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.
Compressed files
newtype CompressedFile
Constructors
CompressedFile | |
compressedFileInvariant :: CompressedFile -> Bool
Invariant for compressed files.
Note that these files are not required to be maximally
compressed, because ranges are allowed to be empty, and the
MetaInfo
s in adjacent ranges are allowed to be equal.
compress :: File -> CompressedFile
Compresses a file by merging consecutive positions with equal meta information into longer ranges.
decompress :: CompressedFile -> File
Decompresses a compressed file.
noHighlightingInRange :: Ranges -> CompressedFile -> CompressedFile
Clear any highlighting info for the given ranges. Used to make sure unsolved meta highlighting overrides error highlighting.
Creation
singletonC :: Ranges -> MetaInfo -> CompressedFile
is a file whose positions are those in singletonC
rs mrs
,
and in which every position is associated with m
.
severalC :: [Ranges] -> MetaInfo -> CompressedFile
Like singletonR
, but with a list of Ranges
instead of a
single one.
splitAtC :: Integer -> CompressedFile -> (CompressedFile, CompressedFile)
splitAtC p f
splits the compressed file f
into (f1, f2)
,
where all the positions in f1
are < p
, and all the positions
in f2
are >= p
.
Inspection
smallestPosC :: CompressedFile -> Maybe Integer
Returns the smallest position, if any, in the CompressedFile
.