Agda.Interaction.Highlighting.Generate

Generates data used for precise syntax highlighting.

Documentation

data Level

Highlighting levels.

Constructors

Full

Full highlighting. Should only be used after typechecking has completed successfully.

Partial

Highlighting without disambiguation of overloaded constructors.

generateAndPrintSyntaxInfo

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

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

generateTokenInfoFromSource

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

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 ()

printErrorInfo :: TCErr -> TCM ()

Prints syntax highlighting info for an error.

errorHighlighting :: TCErr -> TCM File

Generate highlighting for error.

printUnsolvedInfo :: TCM ()

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

printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()

Lispify and print the given highlighting information.

highlightAsTypeChecked

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 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 ()

Highlight a warning.

warningHighlighting :: TCWarning -> File

Generate syntax highlighting for warnings.

computeUnsolvedMetaWarnings :: TCM File

Generates syntax highlighting information for unsolved meta variables.

computeUnsolvedConstraints :: TCM File

Generates syntax highlighting information for unsolved constraints (ideally: that are not connected to a meta variable).

storeDisambiguatedName :: QName -> TCM ()

Remember a name disambiguation (during type checking). To be used later during syntax highlighting.

disambiguateRecordFields

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.