Agda-2.2.4: 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

data TypeCheckingState = TypeCheckingDone | TypeCheckingNotDone generateSyntaxInfo :: FilePath -> TypeCheckingState -> TopLevelInfo -> [([QName], [Range])] -> TCM HighlightingInfo generateErrorInfo :: Range -> String -> File tests :: IO Bool

Documentation

data TypeCheckingState Source

Has typechecking been done yet? Constructors TypeCheckingDone TypeCheckingNotDone Instances Eq TypeCheckingState Show TypeCheckingState

generateSyntaxInfo Source

:: FilePath The module to highlight. -> TypeCheckingState Has it been type checked? -> 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 -> String -> File Source

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

tests :: IO Bool Source

All the properties.

Produced by Haddock version 2.4.2