Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Highlighting.Precise

Contents

- Files
  - Creation
  - Merging
  - Inspection
- Compressed files
  - Creation
  - Inspection
  - Merge

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
  - | CoverageProblem
  - | IncompletePattern
  - | TypeChecks
  - | CatchallClause
- 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

Eq Aspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: Aspect -> Aspect -> Bool Source # (/=) :: Aspect -> Aspect -> Bool Source #
Show Aspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> Aspect -> ShowS Source # show :: Aspect -> String Source # showList :: [Aspect] -> ShowS Source #
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 #

`NameKind`s 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 Source # (/=) :: NameKind -> NameKind -> Bool Source #
Show NameKind Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> NameKind -> ShowS Source # show :: NameKind -> String Source # showList :: [NameKind] -> ShowS Source #
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 `Aspect`s.)

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 Methods minBound :: OtherAspect Source # maxBound :: OtherAspect Source #
Enum OtherAspect Source # |

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

succ :: OtherAspect -> OtherAspect Source #

pred :: OtherAspect -> OtherAspect Source #

toEnum :: Int -> OtherAspect Source #

fromEnum :: OtherAspect -> Int Source #

enumFrom :: OtherAspect -> [OtherAspect] Source #

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect] Source #

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect] Source #

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect] Source #

Eq OtherAspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: OtherAspect -> OtherAspect -> Bool Source # (/=) :: OtherAspect -> OtherAspect -> Bool Source #
Ord OtherAspect Source # |

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

compare :: OtherAspect -> OtherAspect -> Ordering Source #

(<) :: OtherAspect -> OtherAspect -> Bool Source #

(<=) :: OtherAspect -> OtherAspect -> Bool Source #

(>) :: OtherAspect -> OtherAspect -> Bool Source #

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

max :: OtherAspect -> OtherAspect -> OtherAspect Source #

min :: OtherAspect -> OtherAspect -> OtherAspect Source #

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

- 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 Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: DefinitionSite -> DefinitionSite -> Bool Source # (/=) :: DefinitionSite -> DefinitionSite -> Bool Source #
Show DefinitionSite Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> DefinitionSite -> ShowS Source # show :: DefinitionSite -> String Source # showList :: [DefinitionSite] -> ShowS Source #
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

Eq TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: TokenBased -> TokenBased -> Bool Source # (/=) :: TokenBased -> TokenBased -> Bool Source #
Show TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> TokenBased -> ShowS Source # show :: TokenBased -> String Source # showList :: [TokenBased] -> ShowS Source #
Semigroup TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased Source # sconcat :: NonEmpty TokenBased -> TokenBased Source # stimes :: Integral b => b -> TokenBased -> TokenBased Source #
Monoid TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: TokenBased Source # mappend :: TokenBased -> TokenBased -> TokenBased Source # mconcat :: [TokenBased] -> TokenBased Source #
ToJSON TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods toJSON :: TokenBased -> Value Source # toEncoding :: TokenBased -> Encoding Source # toJSONList :: [TokenBased] -> Value Source # toEncodingList :: [TokenBased] -> Encoding Source #
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 #

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

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

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

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