| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |
Symbol | Symbols like forall, =, ->, etc.
PrimitiveType | Things like Set and Prop.
Name (Maybe NameKind) Bool | Is the name an operator part?

Instances

Eq Aspect
Data Aspect
Show Aspect
Typeable Aspect
Arbitrary Aspect
CoArbitrary Aspect
EmbPrj Aspect

data NameKind | Source

Constructors

Bound | Bound variable.
Constructor Induction | Inductive or coinductive constructor.
Datatype |
Field | Record field.
Function |
Module | Module name.
Postulate |
Primitive | Primitive.
Record | Record type.

Instances

Eq NameKind
Data NameKind
Show NameKind
Typeable NameKind
Arbitrary NameKind
CoArbitrary NameKind
EmbPrj NameKind

data OtherAspect | Source

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 `note` explaining why the pattern is incomplete.

Instances

Bounded OtherAspect
Enum OtherAspect
Eq OtherAspect
Data OtherAspect
Show OtherAspect
Typeable OtherAspect
Arbitrary OtherAspect
CoArbitrary OtherAspect
EmbPrj OtherAspect

data MetaInfo | Source

Meta information which can be associated with a character/character range.
Constructors

MetaInfo |

aspect :: Maybe Aspect |
otherAspects :: [OtherAspect] |
note :: Maybe String | This 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.

Instances

Eq MetaInfo
Data MetaInfo
Show MetaInfo
Typeable MetaInfo
Arbitrary MetaInfo
CoArbitrary MetaInfo
Monoid MetaInfo
EmbPrj MetaInfo

data File | Source

A `File` is a mapping from file positions to meta information. The first position in the file has number 1.
Instances

Eq File
Data File
Show File
Typeable File
Arbitrary File
CoArbitrary File
Monoid File

type HighlightingInfo = CompressedFile | Source

Syntax highlighting information for a given source file.

singleton :: Range -> MetaInfo -> File | Source

``singleton` r m` is a file whose positions are those in `r`, and in which every position is associated with `m`.

several :: [Range] -> MetaInfo -> File | Source

Like `singleton`, but with several ranges instead of only one.

smallestPos :: File -> Maybe Integer | Source

Returns the smallest position, if any, in the `File`.

toMap :: File -> Map Integer MetaInfo | Source

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 -> CompressedFile | Source

Compresses a file by merging consecutive positions with equal meta information into longer ranges.

decompress :: CompressedFile -> File | Source

Decompresses a compressed file.

tests :: IO Bool | Source

All the properties.
Produced by Haddock version 2.4.2