Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Highlighting.Precise

Contents

Files
Compressed files

Description

Types used for precise syntax highlighting.

Synopsis

data Aspect
- = Comment
- | Keyword
- | String
- | Number
- | Symbol
- | PrimitiveType
- | Name (Maybe NameKind) Bool
- | Pragma
- | Background
- | Markup
data NameKind
- = Bound
- | Generalizable
- | Constructor Induction
- | Datatype
- | Field
- | Function
- | Module
- | Postulate
- | Primitive
- | Record
- | Argument
- | Macro
data OtherAspect
- = Error
- | DottedPattern
- | UnsolvedMeta
- | UnsolvedConstraint
- | TerminationProblem
- | PositivityProblem
- | Deadcode
- | ShadowingInTelescope
- | CoverageProblem
- | IncompletePattern
- | TypeChecks
- | MissingDefinition
- | CatchallClause
- | ConfluenceProblem
data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: Maybe String
- definitionSite :: Maybe DefinitionSite
- tokenBased :: !TokenBased
}
data DefinitionSite = DefinitionSite {
- defSiteModule :: TopLevelModuleName
- defSitePos :: Int
- defSiteHere :: Bool
- defSiteAnchor :: Maybe String
}
data TokenBased
- = TokenBased
- | NotOnlyTokenBased
newtype File = File {
- mapping :: IntMap Aspects
}
type HighlightingInfo = CompressedFile
parserBased :: Aspects
singleton :: Ranges -> Aspects -> File
several :: [Ranges] -> Aspects -> File
merge :: File -> File -> File
smallestPos :: File -> Maybe Int
toMap :: File -> IntMap Aspects
newtype CompressedFile = CompressedFile {
- ranges :: [(Range, Aspects)]
}
compressedFileInvariant :: CompressedFile -> Bool
compress :: File -> CompressedFile
decompress :: CompressedFile -> File
noHighlightingInRange :: Ranges -> CompressedFile -> CompressedFile
singletonC :: Ranges -> Aspects -> CompressedFile
severalC :: [Ranges] -> Aspects -> CompressedFile
splitAtC :: Int -> CompressedFile -> (CompressedFile, CompressedFile)
selectC :: Range -> CompressedFile -> CompressedFile
smallestPosC :: CompressedFile -> Maybe Int
mergeC :: CompressedFile -> CompressedFile -> CompressedFile

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

Instances details

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

Instances details

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

Instances details

Bounded OtherAspect Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods minBound :: OtherAspect # maxBound :: OtherAspect #
Enum OtherAspect Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise 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 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 Methods compare :: OtherAspect -> OtherAspect -> Ordering # (<) :: OtherAspect -> OtherAspect -> Bool # (<=) :: OtherAspect -> OtherAspect -> Bool # (>) :: OtherAspect -> OtherAspect -> Bool # (>=) :: OtherAspect -> OtherAspect -> Bool # max :: OtherAspect -> OtherAspect -> OtherAspect # min :: OtherAspect -> OtherAspect -> OtherAspect #
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.
tokenBased :: !TokenBased
Is this entry token-based?

Instances

Instances details

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 Methods mempty :: Aspects # mappend :: Aspects -> Aspects -> Aspects # mconcat :: [Aspects] -> Aspects #
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 defSiteModule :: TopLevelModuleName The defining module. defSitePos :: Int The file position in that module. File positions are counted from 1. defSiteHere :: Bool Has this `DefinitionSite` been created at the defining site of the name? defSiteAnchor :: Maybe String A pretty name for the HTML linking.

Instances

Instances details

Eq DefinitionSite Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: DefinitionSite -> DefinitionSite -> Bool # (/=) :: DefinitionSite -> DefinitionSite -> Bool #
Show DefinitionSite Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> DefinitionSite -> ShowS # show :: DefinitionSite -> String # showList :: [DefinitionSite] -> ShowS #
EmbPrj DefinitionSite Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Int32 Source # icod_ :: DefinitionSite -> S Int32 Source # value :: Int32 -> R DefinitionSite Source #

data TokenBased Source #

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

Constructors

TokenBased
NotOnlyTokenBased

Instances

Instances details

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 Methods mempty :: TokenBased # mappend :: TokenBased -> TokenBased -> TokenBased # mconcat :: [TokenBased] -> TokenBased #
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
EncodeTCM TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods encodeTCM :: TokenBased -> TCM Value Source #

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 mapping :: IntMap Aspects

Instances

Instances details

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 ranges :: [(Range, Aspects)]

Instances

Instances details

Eq CompressedFile Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: CompressedFile -> CompressedFile -> Bool # (/=) :: CompressedFile -> CompressedFile -> Bool #
Show CompressedFile Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> CompressedFile -> ShowS # show :: CompressedFile -> String # showList :: [CompressedFile] -> ShowS #
Semigroup CompressedFile Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: CompressedFile -> CompressedFile -> CompressedFile # sconcat :: NonEmpty CompressedFile -> CompressedFile # stimes :: Integral b => b -> CompressedFile -> CompressedFile #
Monoid CompressedFile Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: CompressedFile # mappend :: CompressedFile -> CompressedFile -> CompressedFile # mconcat :: [CompressedFile] -> CompressedFile #
EmbPrj CompressedFile Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: CompressedFile -> S Int32 Source # icod_ :: CompressedFile -> S Int32 Source # value :: Int32 -> R CompressedFile Source #

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.

selectC :: Range -> CompressedFile -> CompressedFile Source #

Inspection

smallestPosC :: CompressedFile -> Maybe Int Source #

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

Merge

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

Merges compressed files.