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

Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Highlighting.Precise

Contents

Description

Types used for precise syntax highlighting.

Synopsis

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 # 

Methods

(==) :: Aspect -> Aspect -> Bool #

(/=) :: Aspect -> Aspect -> Bool #

Show 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}

Macro

Macro.

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 
PositivityProblem 
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 #

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

Constructors

Aspects 

Fields

newtype File #

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

The first position in the file has number 1.

Constructors

File 

Instances

Eq File # 

Methods

(==) :: File -> File -> Bool #

(/=) :: File -> File -> Bool #

Show File # 

Methods

showsPrec :: Int -> File -> ShowS #

show :: File -> String #

showList :: [File] -> ShowS #

Semigroup File # 

Methods

(<>) :: File -> File -> File #

sconcat :: NonEmpty File -> File #

stimes :: Integral b => b -> File -> File #

Monoid File # 

Methods

mempty :: File #

mappend :: File -> File -> File #

mconcat :: [File] -> 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.

Merging

merge :: File -> File -> File #

Merges files.

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

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.

Merge

mergeC :: CompressedFile -> CompressedFile -> CompressedFile #

Merges compressed files.