Generates data used for precise syntax highlighting.
- data Level
- generateAndPrintSyntaxInfo :: Declaration -> Level -> TCM ()
- generateTokenInfo :: AbsolutePath -> TCM CompressedFile
- printErrorInfo :: TCErr -> TCM ()
- printUnsolvedInfo :: TCM ()
- printHighlightingInfo :: MonadTCM tcm => HighlightingInfo -> tcm ()
- highlightAsTypeChecked :: MonadTCM tcm => Range -> Range -> tcm a -> tcm a
- tests :: IO Bool
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.
Highlighting without disambiguation of overloaded constructors.
Generate syntax highlighting information for the given
declaration, and (if appropriate) print it. If the
, 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
then this token highlighting info is additionally removed from
Generate and return the syntax highlighting information for the tokens in the given file.
Generates and prints syntax highlighting information for unsolved meta-variables and certain unsolved constraints.
Lispify and print the given highlighting information.
highlightAsTypeChecked rPre r m runs
m and returns its
result. Some code may additionally be highlighted:
ris non-empty and not a sub-range of
continuousPerLinehas been applied to both):
ris highlighted as being type-checked while
mis running (this highlighting is removed if
- Otherwise: Highlighting is removed for
rPre - rbefore
mruns, and if
mcompletes successfully, then
rPre - ris highlighted as being type-checked.