print package:Agda

Prints the accumulated benchmark results. Does nothing if no benchmark profiling is enabled.

Prints syntax highlighting info for an error.

Lispify and print the given highlighting information.

Generates and prints syntax highlighting information for unsolved meta-variables and certain unsolved constraints.

Print usage information.

Print version information.

Prints out the path to the Agda mode's main file (using UTF-8 and without any trailing newline).

Debug print the scope.

Print the given statistics.

Print Agda version number.

Options --version and --numeric-version (last wins).

Print Agda version information.

Wrapper to indicate that range should be printed.

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.