Agda-2.8.0: 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 HighlightingInfo
- generateTokenInfoFromSource :: RangeFile -> String -> TCM HighlightingInfo
- generateTokenInfoFromString :: Range -> String -> TCM HighlightingInfo
- printSyntaxInfo :: Range -> TCM ()
- printErrorInfo :: TCErr -> TCM ()
- errorHighlighting :: TCErr -> TCM HighlightingInfoBuilder
- printUnsolvedInfo :: TCM ()
- printHighlightingInfo :: MonadTrace m => RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
- highlightAsTypeChecked :: MonadTrace m => Range -> Range -> m a -> m a
- highlightWarning :: TCWarning -> TCM ()
- warningHighlighting :: TCWarning -> HighlightingInfoBuilder
- computeUnsolvedInfo :: TCM HighlightingInfoBuilder
- storeDisambiguatedConstructor :: Induction -> QName -> TCM ()
- storeDisambiguatedProjection :: 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 | Declaration to highlight.
-> Level | Amount of highlighting.
-> 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 highlighting info corresponding to `stTokens` (that corresponding to the interval covered by the declaration). If the boolean is `True`, then this highlighting info is additionally removed from the data structure that `stTokens` refers to.

generateTokenInfo :: AbsolutePath -> TCM HighlightingInfo Source #

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

generateTokenInfoFromSource Source #

Arguments

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

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

generateTokenInfoFromString :: Range -> String -> TCM HighlightingInfo 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 HighlightingInfoBuilder Source #

Generate highlighting for error.

printUnsolvedInfo :: TCM () Source #

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

printHighlightingInfo :: MonadTrace m => RemoveTokenBasedHighlighting -> HighlightingInfo -> m () Source #

Lispify and print the given highlighting information.

highlightAsTypeChecked Source #

Arguments

:: MonadTrace m |

=> Range

    rPre

-> Range

    r

-> m a |
-> m a |

`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.

highlightWarning :: TCWarning -> TCM () Source #

Highlight a warning. We do not generate highlighting for unsolved metas and constraints, as that gets handled in bulk after typechecking.

warningHighlighting :: TCWarning -> HighlightingInfoBuilder Source #

Generate syntax highlighting for warnings.

computeUnsolvedInfo :: TCM HighlightingInfoBuilder Source #

storeDisambiguatedConstructor :: Induction -> QName -> TCM () Source #

storeDisambiguatedProjection :: QName -> TCM () Source #

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.