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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Highlighting.Generate

Description

Generates data used for precise syntax highlighting.

Synopsis

- data Level
  - = Full
  - | Partial
- generateAndPrintSyntaxInfo :: Declaration -> Level -> Bool -> TCM ()
- generateTokenInfo :: AbsolutePath -> TCM CompressedFile
- generateTokenInfoFromSource :: AbsolutePath -> String -> TCM CompressedFile
- generateTokenInfoFromString :: Range -> String -> TCM CompressedFile
- printSyntaxInfo :: Range -> TCM ()
- printErrorInfo :: TCErr -> TCM ()
- errorHighlighting :: TCErr -> TCM File
- printUnsolvedInfo :: TCM ()
- printHighlightingInfo :: MonadTCM tcm => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
- highlightAsTypeChecked :: MonadTCM tcm => Range -> Range -> tcm a -> tcm a
- warningHighlighting :: TCWarning -> File
- computeUnsolvedMetaWarnings :: TCM File
- computeUnsolvedConstraints :: TCM File
- storeDisambiguatedName :: QName -> TCM ()
- disambiguateRecordFields :: [Name] -> [QName] -> TCM ()

# Documentation

data Level Source #

Highlighting levels.

Constructors

Full | Full highlighting. Should only be used after typechecking has completed successfully.
Partial | Highlighting without disambiguation of overloaded constructors.

generateAndPrintSyntaxInfo Source #

Arguments

:: Declaration |
-> Level |
-> Bool | Update the state?
-> TCM () |

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

generateTokenInfo :: AbsolutePath -> TCM CompressedFile Source #

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

generateTokenInfoFromSource Source #

Arguments

:: AbsolutePath | The module to highlight.
-> String | The file contents. Note that the file is not read from disk.
-> TCM CompressedFile |

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

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

Generate and return the syntax highlighting information for the tokens in the given string, which is assumed to correspond to the given range.

printSyntaxInfo :: Range -> TCM () Source #

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

warningHighlighting :: TCWarning -> File Source #

Generate syntax highlighting for warnings.

computeUnsolvedMetaWarnings :: TCM File Source #

Generates syntax highlighting information for unsolved meta variables.

computeUnsolvedConstraints :: TCM File Source #

Generates syntax highlighting information for unsolved constraints (ideally: 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.

disambiguateRecordFields Source #

Arguments

:: [Name] | Record field names in a record expression.
-> [QName] | Record field names in the corresponding record type definition
-> TCM () |

Store a disambiguation of record field tags for the purpose of highlighting.