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

Methods

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

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

Show Aspect

Methods

showsPrec :: Int -> Aspect -> ShowS

show :: Aspect -> String

showList :: [Aspect] -> ShowS

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.

Instances

Eq NameKind

Methods

(==) :: NameKind -> NameKind -> Bool

(/=) :: NameKind -> NameKind -> Bool

Show NameKind

Methods

showsPrec :: Int -> NameKind -> ShowS

show :: NameKind -> String

showList :: [NameKind] -> ShowS

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.

Instances

Bounded OtherAspect

Methods

minBound :: OtherAspect

maxBound :: OtherAspect

Enum OtherAspect

Methods

succ :: OtherAspect -> OtherAspect

pred :: OtherAspect -> OtherAspect

toEnum :: Int -> OtherAspect

fromEnum :: OtherAspect -> Int

enumFrom :: OtherAspect -> [OtherAspect]

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]

Eq OtherAspect

Methods

(==) :: OtherAspect -> OtherAspect -> Bool

(/=) :: OtherAspect -> OtherAspect -> Bool

Show OtherAspect

Methods

showsPrec :: Int -> OtherAspect -> ShowS

show :: OtherAspect -> String

showList :: [OtherAspect] -> ShowS

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

Methods

(==) :: Aspects -> Aspects -> Bool

(/=) :: Aspects -> Aspects -> Bool

Show Aspects

Methods

showsPrec :: Int -> Aspects -> ShowS

show :: Aspects -> String

showList :: [Aspects] -> ShowS

Semigroup Aspects

Methods

(<>) :: Aspects -> Aspects -> Aspects

sconcat :: NonEmpty Aspects -> Aspects

stimes :: Integral b => b -> Aspects -> Aspects

Monoid Aspects

Methods

mempty :: Aspects

mappend :: Aspects -> Aspects -> Aspects

mconcat :: [Aspects] -> Aspects

newtype File

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

The first position in the file has number 1.

Constructors

File

Fields

• mapping :: IntMap Aspects

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

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

Methods

(==) :: CompressedFile -> CompressedFile -> Bool

(/=) :: CompressedFile -> CompressedFile -> Bool

Show CompressedFile

Methods

showsPrec :: Int -> CompressedFile -> ShowS

show :: CompressedFile -> String

showList :: [CompressedFile] -> ShowS

Semigroup CompressedFile

Methods

(<>) :: CompressedFile -> CompressedFile -> CompressedFile

sconcat :: NonEmpty CompressedFile -> CompressedFile

stimes :: Integral b => b -> CompressedFile -> CompressedFile

Monoid CompressedFile

Methods

mempty :: CompressedFile

mappend :: CompressedFile -> CompressedFile -> CompressedFile

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

selectC :: Range -> CompressedFile -> CompressedFile

Inspection

smallestPosC :: CompressedFile -> Maybe Int

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

Merge

mergeC :: CompressedFile -> CompressedFile -> CompressedFile

Merges compressed files.