Agda-2.6.0.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

Instances
Eq Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

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

Show Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> Aspect -> ShowS

show :: Aspect -> String

showList :: [Aspect] -> ShowS

EmbPrj Aspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32 Source #

icod_ :: Aspect -> S Int32 Source #

value :: Int32 -> R Aspect Source #

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.

Instances
Eq NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

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

Show NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> NameKind -> ShowS

show :: NameKind -> String

showList :: [NameKind] -> ShowS

EmbPrj NameKind Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32 Source #

icod_ :: NameKind -> S Int32 Source #

value :: Int32 -> R NameKind Source #

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.

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. NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode.

CatchallClause 
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

Methods

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

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

Ord OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Show OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> OtherAspect -> ShowS

show :: OtherAspect -> String

showList :: [OtherAspect] -> ShowS

EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32 Source #

icod_ :: OtherAspect -> S Int32 Source #

value :: Int32 -> R OtherAspect Source #

data Aspects Source #

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

Constructors

Aspects 

Fields

  • aspect :: Maybe Aspect
     
  • otherAspects :: Set 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 DefinitionSite

    The definition site of the annotated thing, if applicable and known. File positions are counted from 1.

  • tokenBased :: !TokenBased

    Is this entry token-based?

Instances
Eq Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

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

Show Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> Aspects -> ShowS

show :: Aspects -> String

showList :: [Aspects] -> ShowS

Semigroup Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty Aspects -> Aspects

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

Monoid Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32 Source #

icod_ :: Aspects -> S Int32 Source #

value :: Int32 -> R Aspects Source #

data DefinitionSite Source #

Constructors

DefinitionSite 

Fields

data TokenBased Source #

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

Instances
Eq TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

(==) :: TokenBased -> TokenBased -> Bool

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

Show TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> TokenBased -> ShowS

show :: TokenBased -> String

showList :: [TokenBased] -> ShowS

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: TokenBased -> TokenBased -> TokenBased

sconcat :: NonEmpty TokenBased -> TokenBased

stimes :: Integral b => b -> TokenBased -> TokenBased

Monoid TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32 Source #

icod_ :: TokenBased -> S Int32 Source #

value :: Int32 -> R TokenBased Source #

ToJSON TokenBased 
Instance details

Defined in Agda.Interaction.Highlighting.JSON

Methods

toJSON :: TokenBased -> Value

toEncoding :: TokenBased -> Encoding

toJSONList :: [TokenBased] -> Value

toEncodingList :: [TokenBased] -> Encoding

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 

Fields

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

parserBased :: Aspects Source #

A variant of mempty with tokenBased set to NotOnlyTokenBased.

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

newtype CompressedFile Source #

A compressed File, in which consecutive positions with the same Aspects are stored together.

Constructors

CompressedFile 

Fields

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.