Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.Highlighting.Precise
Description
Types used for precise syntax highlighting.
Synopsis
data Aspect
= Comment
| Keyword
| String
| Number
| Symbol
| PrimitiveType
| Name (Maybe NameKind) Bool
data NameKind
= Bound
| Constructor Induction
| Datatype
| Field
| Function
| Module
| Postulate
| Primitive
| Record
data OtherAspect
= Error
| DottedPattern
| UnsolvedMeta
| TerminationProblem
| IncompletePattern
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 Source
Various more or less syntactic aspects of the code. (These cannot overlap.)
Constructors
Comment
Keyword
String
Number
SymbolSymbols like forall, =, ->, etc.
PrimitiveTypeThings like Set and Prop.
Name (Maybe NameKind) BoolIs the name an operator part?
data NameKind Source
Constructors
BoundBound variable.
Constructor InductionInductive or coinductive constructor.
Datatype
FieldRecord field.
Function
ModuleModule name.
Postulate
PrimitivePrimitive.
RecordRecord type.
data OtherAspect Source
Other aspects. (These can overlap with each other and with Aspects.)
Constructors
Error
DottedPattern
UnsolvedMeta
TerminationProblem
IncompletePatternWhen this constructor is used it is probably a good idea to include a note explaining why the pattern is incomplete.
data MetaInfo Source
Meta information which can be associated with a character/character range.
Constructors
MetaInfo
aspect :: Maybe Aspect
otherAspects :: [OtherAspect]
note :: Maybe StringThis 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.
data File Source

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 m is a file whose positions are those in r, and in which every position is associated with m.
several :: [Range] -> MetaInfo -> FileSource
Like singleton, but with several ranges instead of only one.
smallestPos :: File -> Maybe IntegerSource
Returns the smallest position, if any, in the File.
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
A compressed File, in which consecutive positions with the same MetaInfo are stored together.
compress :: File -> CompressedFileSource
Compresses a file by merging consecutive positions with equal meta information into longer ranges.
decompress :: CompressedFile -> FileSource
Decompresses a compressed file.
tests :: IO BoolSource
All the properties.
Produced by Haddock version 2.6.0