Safe Haskell	None
Language	Haskell98

Agda.Interaction.Highlighting.Precise

Contents

Files
- Creation
- Inspection
Compressed files
- Creation
- Inspection
Tests

Description

Types used for precise syntax highlighting.

Synopsis

Files

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
Show Aspect
Arbitrary Aspect
CoArbitrary Aspect
EmbPrj Aspect
Typeable * 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.
Argument	Named argument, like x in {x = v}

Instances

Eq NameKind
Show NameKind
Arbitrary NameKind
CoArbitrary NameKind
EmbPrj NameKind
Typeable * NameKind

data OtherAspect Source

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
Arbitrary OtherAspect
CoArbitrary OtherAspect
EmbPrj OtherAspect
Typeable * OtherAspect

data MetaInfo Source

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
Arbitrary MetaInfo
CoArbitrary MetaInfo
Monoid MetaInfo
EmbPrj MetaInfo
Typeable * 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
Show File
Arbitrary File
CoArbitrary File
Monoid File
Typeable * File

type HighlightingInfo = CompressedFile Source

Syntax highlighting information.

Creation

singleton :: Ranges -> MetaInfo -> File Source

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 Source

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

Inspection

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.

Compressed files

newtype CompressedFile Source

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
Arbitrary CompressedFile
Monoid CompressedFile
EmbPrj CompressedFile
Typeable * CompressedFile

compressedFileInvariant :: CompressedFile -> Bool Source

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 Source

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

decompress :: CompressedFile -> File Source

Decompresses a compressed file.

noHighlightingInRange :: Ranges -> CompressedFile -> CompressedFile Source

Clear any highlighting info for the given ranges. Used to make sure unsolved meta highlighting overrides error highlighting.

Creation

singletonC :: Ranges -> MetaInfo -> CompressedFile Source

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 Source

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

splitAtC :: Integer -> CompressedFile -> (CompressedFile, CompressedFile) Source

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 Source

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

Tests

tests :: IO Bool Source

All the properties.