Agda-2.6.1: 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 Source #

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?

Pragma

Text occurring in pragmas that does not have a more specific aspect.

Background

Non-code contents in literate Agda

Markup

Delimiters used to separate the Agda code blocks from the other contents in literate Agda

data NameKind Source #

NameKinds are figured out during scope checking.

Constructors

Bound

Bound variable.

Generalizable

Generalizable variable. (This includes generalizable variables that have been generalized).

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

Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc.

ShadowingInTelescope

Used for shadowed repeated variable names in telescopes.

CoverageProblem 
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.

MissingDefinition

Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode.

CatchallClause 
ConfluenceProblem 
Instances
Bounded OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Enum OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Eq OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Ord OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Show OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

data Aspects Source #

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

Constructors

Aspects 

Fields

data DefinitionSite Source #

Constructors

DefinitionSite 

Fields

data TokenBased Source #

Is the highlighting "token-based", i.e. based only on information from the lexer?

newtype File Source #

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 Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

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

Show File Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> File -> ShowS #

show :: File -> String #

showList :: [File] -> ShowS #

Semigroup File Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty File -> File #

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

Monoid File Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: File #

mappend :: File -> File -> File #

mconcat :: [File] -> File #

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.

Merging

merge :: File -> File -> File Source #

Merges files.

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

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.

Merge

mergeC :: CompressedFile -> CompressedFile -> CompressedFile Source #

Merges compressed files.