Agda.Interaction.Highlighting.Precise

Types used for precise syntax highlighting.

Files

data Aspect

Syntactic aspects of the code. (These cannot overlap.) They can be obtained from the lexed tokens already, except for the NameKind.

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

CoArbitrary Aspect

Arbitrary Aspect

EmbPrj Aspect

data NameKind

NameKinds are figured our during scope checking.

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

CoArbitrary NameKind

Arbitrary NameKind

EmbPrj NameKind

data OtherAspect

Other aspects, generated by type checking. (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

CoArbitrary OtherAspect

Arbitrary OtherAspect

EmbPrj OtherAspect

data Aspects

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

Constructors

Aspects

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, Int)

The definition site of the annotated thing, if applicable and known. File positions are counted from 1.

Instances

Eq Aspects

Show Aspects

Monoid Aspects

CoArbitrary Aspects

Arbitrary Aspects

EmbPrj Aspects

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

Monoid File

CoArbitrary File

Arbitrary File

type HighlightingInfo = CompressedFile

Syntax highlighting information.

Creation

singleton :: Ranges -> Aspects -> File

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

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

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

Inspection

smallestPos :: File -> Maybe Int

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

toMap :: File -> IntMap Aspects

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 Aspects are stored together.

Constructors

CompressedFile

Fields

ranges :: [(Range, Aspects)]

Instances

Eq CompressedFile

Show CompressedFile

Monoid CompressedFile

Arbitrary 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 Aspectss 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 -> Aspects -> CompressedFile

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

severalC :: [Ranges] -> Aspects -> CompressedFile

Like singletonR, but with a list of Ranges instead of a single one.

splitAtC :: Int -> 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 Int

Returns the smallest position, if any, in the CompressedFile.

Tests

tests :: IO Bool

All the properties.