Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Highlighting.Precise

Contents

Files
Compressed files

Description

Types used for precise syntax highlighting.

Synopsis

data Aspect
- = Comment
- | Option
- | Keyword
- | String
- | Number
- | Symbol
- | PrimitiveType
- | Name (Maybe NameKind) Bool
data NameKind
- = Bound
- | Constructor Induction
- | Datatype
- | Field
- | Function
- | Module
- | Postulate
- | Primitive
- | Record
- | Argument
- | Macro
data OtherAspect
- = Error
- | DottedPattern
- | UnsolvedMeta
- | UnsolvedConstraint
- | TerminationProblem
- | PositivityProblem
- | ReachabilityProblem
- | CoverageProblem
- | IncompletePattern
- | CatchallClause
- | TypeChecks
data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: [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 #

Syntactic aspects of the code. (These cannot overlap.) They can be obtained from the lexed tokens already, except for the NameKind.

Constructors

Comment
Option
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 #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: Aspect -> Aspect -> Bool # (/=) :: Aspect -> Aspect -> Bool #
Show Aspect #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> Aspect -> ShowS # show :: Aspect -> String # showList :: [Aspect] -> ShowS #
EmbPrj Aspect #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Int32 # icod_ :: Aspect -> S Int32 # value :: Int32 -> R Aspect #

data NameKind #

NameKinds are figured out 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 #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: NameKind -> NameKind -> Bool # (/=) :: NameKind -> NameKind -> Bool #
Show NameKind #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> NameKind -> ShowS # show :: NameKind -> String # showList :: [NameKind] -> ShowS #
EmbPrj NameKind #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Int32 # icod_ :: NameKind -> S Int32 # value :: Int32 -> R NameKind #

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
ReachabilityProblem
CoverageProblem
IncompletePattern	When this constructor is used it is probably a good idea to include a `note` explaining why the pattern is incomplete.
CatchallClause
TypeChecks	Code which is being type-checked.

Instances

Bounded OtherAspect #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods minBound :: OtherAspect # maxBound :: OtherAspect #
Enum OtherAspect #
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 #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: OtherAspect -> OtherAspect -> Bool # (/=) :: OtherAspect -> OtherAspect -> Bool #
Show OtherAspect #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> OtherAspect -> ShowS # show :: OtherAspect -> String # showList :: [OtherAspect] -> ShowS #
EmbPrj OtherAspect #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Int32 # icod_ :: OtherAspect -> S Int32 # value :: Int32 -> R OtherAspect #

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

data DefinitionSite #

Constructors

DefinitionSite
Fields defSiteModule :: TopLevelModuleName The defining module. defSitePos :: Int The file position in that module. 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

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

data TokenBased #

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

Constructors

TokenBased
NotOnlyTokenBased

Instances

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

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 #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: File -> File -> Bool # (/=) :: File -> File -> Bool #
Show File #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> File -> ShowS # show :: File -> String # showList :: [File] -> ShowS #
Semigroup File #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: File -> File -> File # sconcat :: NonEmpty File -> File # stimes :: Integral b => b -> File -> File #
Monoid File #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: File # mappend :: File -> File -> File # mconcat :: [File] -> File #

type HighlightingInfo = CompressedFile #

Syntax highlighting information.

Creation

parserBased :: Aspects #

A variant of mempty with tokenBased set to NotOnlyTokenBased.

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