| 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 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, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
- highlightAsTypeChecked :: (MonadTCM tcm, ReadTCState tcm) => Range -> Range -> tcm a -> tcm a
- highlightWarning :: TCWarning -> TCM ()
- warningHighlighting :: TCWarning -> File
- computeUnsolvedMetaWarnings :: TCM File
- computeUnsolvedConstraints :: TCM File
- storeDisambiguatedName :: QName -> TCM ()
- disambiguateRecordFields :: [Name] -> [QName] -> TCM ()
Documentation
Highlighting levels.
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.
printUnsolvedInfo :: TCM () Source #
Generates and prints syntax highlighting information for unsolved meta-variables and certain unsolved constraints.
printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm () Source #
Lispify and print the given highlighting information.
highlightAsTypeChecked Source #
Arguments
| :: (MonadTCM tcm, ReadTCState tcm) | |
| => Range | rPre |
| -> Range | r |
| -> tcm a | |
| -> tcm 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.
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.