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

Safe Haskell | None

Agda.Interaction.Highlighting.Generate

Description

Generates data used for precise syntax highlighting.

Synopsis

- data Level
  - = Full [TerminationError]
  - | Partial
- generateAndPrintSyntaxInfo :: Declaration -> Level -> TCM ()
- generateTokenInfo :: AbsolutePath -> TCM CompressedFile
- printErrorInfo :: TCErr -> TCM ()
- printUnsolvedInfo :: TCM ()
- printHighlightingInfo :: MonadTCM tcm => HighlightingInfo -> tcm ()
- highlightAsTypeChecked :: MonadTCM tcm => Range -> Range -> tcm a -> tcm a
- tests :: IO Bool

# Documentation

data Level

Highlighting levels.

Constructors

Full [TerminationError] | Full highlighting. Should only be used after typechecking has completed successfully. The list of termination problems is also highlighted. Precondition: The termination problems must be located in the module that is highlighted.
Partial | Highlighting without disambiguation of overloaded constructors.

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

Generate syntax highlighting information for the given declaration, and (if appropriate) print it. If the `HighlightingLevel` is ``Full` something`, 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` something`, then this token highlighting info is additionally removed from `stTokens`.

generateTokenInfo

Arguments

:: AbsolutePath | The module to highlight.
-> TCM CompressedFile |

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

printErrorInfo :: TCErr -> TCM ()

Prints syntax highlighting info for an error.

printUnsolvedInfo :: TCM ()

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

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

Lispify and print the given highlighting information.

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

`highlightAsTypeChecked rPre r m` runs `m` and returns its result. Some code may additionally 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.

tests :: IO Bool

All the properties.