Agda.Interaction.Highlighting.Generate

Generates data used for precise syntax highlighting.

Documentation

data Level

Highlighting levels.

Constructors

Full [TerminationError]

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

The list of termination problems is also highlighted.

Precondition: The termination problems must be located in the module that is highlighted.

Partial

Highlighting without disambiguation of overloaded constructors.

generateAndPrintSyntaxInfo :: Declaration -> Level -> TCM ()

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

generateTokenInfo

Arguments

:: AbsolutePath

The module to highlight.

-> TCM CompressedFile

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

printErrorInfo :: TCErr -> TCM ()

Prints syntax highlighting info for an error.

printUnsolvedInfo :: TCM ()

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

printHighlightingInfo :: MonadTCM tcm => HighlightingInfo -> tcm ()

Lispify and print the given highlighting information.

highlightAsTypeChecked :: MonadTCM tcm => Range -> Range -> tcm a -> tcm a

highlightAsTypeChecked rPre r m runs m and returns its result. Some code may additionally 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.

tests :: IO Bool

All the properties.