Agda-2.4.2.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Interaction.Highlighting.Precise

Contents

Description

Types used for precise syntax highlighting.

Synopsis

Files

data Aspect Source

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

data NameKind Source

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}

data OtherAspect Source

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.

data Aspects Source

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.

data File Source

A File is a mapping from file positions to meta information.

The first position in the file has number 1.

Instances

type HighlightingInfo = CompressedFile Source

Syntax highlighting information.

Creation

singleton :: Ranges -> Aspects -> 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] -> Aspects -> File Source

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

Inspection

smallestPos :: File -> Maybe Int Source

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

toMap :: File -> IntMap Aspects 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 Aspects are stored together.

Constructors

CompressedFile 

Fields

ranges :: [(Range, Aspects)]
 

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 Aspectss 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 -> Aspects -> 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] -> Aspects -> CompressedFile Source

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

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

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

Tests

tests :: IO Bool Source

All the properties.