Agda.Interaction.Highlighting.Precise

Types used for precise syntax highlighting.

Files

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

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.

Argument

Named argument, like x in {x = v}

Instances

Eq 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

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

TypeChecks

Code which is being type-checked.

Instances

Bounded OtherAspect

Enum OtherAspect

Eq 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

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

Show File

Typeable File

Arbitrary File

CoArbitrary File

Monoid File

type HighlightingInfo = CompressedFile

Syntax highlighting information.

Creation

singleton :: Ranges -> MetaInfo -> File

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

several :: [Ranges] -> MetaInfo -> File

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

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

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

Constructors

CompressedFile

Fields

ranges :: [(Range, MetaInfo)]

Instances

Eq CompressedFile

Show CompressedFile

Typeable CompressedFile

Arbitrary CompressedFile

Monoid CompressedFile

EmbPrj 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 MetaInfos 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

singletonC rs m is a file whose positions are those in rs, 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.

Tests

tests :: IO Bool

All the properties.