Agda.Interaction.Highlighting.Precise

Types used for precise syntax highlighting.

Documentation

data Aspect

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

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

Other aspects. (These can overlap with each other and with Aspects.)

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

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

Constructors

MetaInfo

Fields

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

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

Syntax highlighting information for a given source file.

singleton :: Range -> MetaInfo -> File

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

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

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)]

A compressed File, in which consecutive positions with the same MetaInfo are stored together.

compress :: File -> CompressedFile

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

decompress :: CompressedFile -> File

Decompresses a compressed file.

tests :: IO Bool

All the properties.