| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Interaction.Highlighting.Generate

Description
Generates data used for precise syntax highlighting.
Synopsis

generateSyntaxInfo :: AbsolutePath -> Maybe TCErr -> TopLevelInfo -> [([QName], [Range])] -> TCM HighlightingInfo
generateErrorInfo :: Range -> Maybe String -> Maybe HighlightingInfo
tests :: IO Bool

Documentation

generateSyntaxInfo | Source

:: 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.
-> [([QName], [Range])] | Functions which failed to termination check (grouped if they are mutual), along with ranges for problematic call sites.
-> TCM HighlightingInfo |
Generates syntax highlighting information.

generateErrorInfo :: Range -> Maybe String -> Maybe HighlightingInfo | Source

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 Bool | Source

All the properties.
Produced by Haddock version 2.4.2