Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Generates data used for precise syntax highlighting.



data Level Source

Highlighting levels.



Full highlighting. Should only be used after typechecking has completed successfully.


Highlighting without disambiguation of overloaded constructors.

generateAndPrintSyntaxInfo :: Declaration -> Level -> TCM () Source

Generate syntax highlighting information for the given declaration, and (if appropriate) print it. If the HighlightingLevel is Full, then the state is additionally updated with the new highlighting info (in case of a conflict new info takes precedence over old info).

The procedure makes use of some of the token highlighting info in stTokens (that corresponding to the interval covered by the declaration). If the HighlightingLevel is Full, then this token highlighting info is additionally removed from stTokens.

generateTokenInfo Source


:: AbsolutePath

The module to highlight.

-> TCM CompressedFile 

Generate and return the syntax highlighting information for the tokens in the given file.

generateTokenInfoFromString :: Range -> String -> TCM CompressedFile Source

Same as generateTokenInfo but takes a string instead of a filename.

printErrorInfo :: TCErr -> TCM () Source

Prints syntax highlighting info for an error.

errorHighlighting :: TCErr -> TCM File Source

Generate highlighting for error. Does something special for termination errors.

printUnsolvedInfo :: TCM () Source

Generates and prints syntax highlighting information for unsolved meta-variables and certain unsolved constraints.

printHighlightingInfo :: MonadTCM tcm => HighlightingInfo -> tcm () Source

Lispify and print the given highlighting information.

highlightAsTypeChecked :: MonadTCM tcm => Range -> Range -> tcm a -> tcm a Source

highlightAsTypeChecked rPre r m runs m and returns its result. Additionally, some code may be highlighted:

  • If r is non-empty and not a sub-range of rPre (after continuousPerLine has been applied to both): r is highlighted as being type-checked while m is running (this highlighting is removed if m completes successfully).
  • Otherwise: Highlighting is removed for rPre - r before m runs, and if m completes successfully, then rPre - r is highlighted as being type-checked.

computeUnsolvedMetaWarnings :: TCM File Source

Generates syntax highlighting information for unsolved meta variables.

computeUnsolvedConstraints :: TCM File Source

Generates syntax highlighting information for unsolved constraints that are not connected to a meta variable.

storeDisambiguatedName :: QName -> TCM () Source

Remember a name disambiguation (during type checking). To be used later during syntax highlighting.

tests :: IO Bool Source

All the properties.