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?
show/hide Instances
data NameKind Source
Constructors
BoundBound variable.
Constructor InductionInductive or coinductive constructor.
Datatype
FieldRecord field.
Function
ModuleModule name.
Postulate
PrimitivePrimitive.
RecordRecord type.
show/hide Instances
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.
show/hide Instances
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.
show/hide Instances
data File Source

A File is a mapping from file positions to meta information.

The first position in the file has number 1.

show/hide Instances
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.4.2