Agda.Interaction.Highlighting.Generate

Highlighting levels.

Generate syntax highlighting information for the given declaration, and (if appropriate) print it. If the boolean is True, 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 highlighting info corresponding to stTokens (that corresponding to the interval covered by the declaration). If the boolean is True, then this highlighting info is additionally removed from the data structure that stTokens refers to.

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

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

Generate and return the syntax highlighting information for the tokens in the given string, which is assumed to correspond to the given range.

Prints syntax highlighting info for an error.

Generate highlighting for error.

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. Additionally, some code may 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.

Highlight a warning. We do not generate highlighting for unsolved metas and constraints, as that gets handled in bulk after typechecking.

Generate syntax highlighting for warnings.

Store a disambiguation of record field tags for the purpose of highlighting.