| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Highlighting.Generate
Description
Generates data used for precise syntax highlighting.
Synopsis
- data Level
- 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
Highlighting levels.
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
ris non-empty and not a sub-range ofrPre(aftercontinuousPerLinehas been applied to both):ris highlighted as being type-checked whilemis running (this highlighting is removed ifmcompletes successfully). - Otherwise: Highlighting is removed for
rPre - rbeforemruns, and ifmcompletes successfully, thenrPre - ris 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.
storeDisambiguatedProjection :: QName -> TCM () Source #