Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.Interaction.Highlighting.Generate

Description

Generates data used for precise syntax highlighting.

Synopsis

Documentation

generateSyntaxInfoSource

Arguments

:: AbsolutePath

The module to highlight.

-> Maybe TCErr

Nothing if the module has been successfully type checked (perhaps with warnings), otherwise the offending error.

Precondition: The range of the error must match the file name given in the previous argument.

-> TopLevelInfo

The abstract syntax of the module.

-> [TerminationError]

Termination checking problems.

-> TCM HighlightingInfo 

Generates syntax highlighting information.

generateErrorInfo :: Range -> Maybe String -> Maybe HighlightingInfoSource

Generates syntax highlighting information for an error, represented as a range and an optional string. The error range is completed so that there are no gaps in it.

Nothing is generated unless the file name component of the range is defined.

tests :: IO BoolSource

All the properties.