Token package:Agda

The most general way of parsing a token.

Parses a single token.

Is the highlighting "token-based", i.e. based only on information from the lexer?

Is this entry token-based?

Gives the parsed token stream (including comments).

Parse the token stream. Used by the TeX compiler.

Tells Agda to compute token-based highlighting information for the file. This command works even if the file's module name does not match its location in the file system, or if the file is not scope-correct. Furthermore no file names are put in the generated output. Thus it is fine to put source code into a temporary file before calling this command. However, the file extension should be correct. If the second argument is Remove, then the (presumably temporary) file is removed after it has been read.

Formats the TokenBased tag for the Emacs backend. No quotes are added.

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.

Should token-based highlighting be removed in conjunction with the application of new highlighting (in order to reduce the risk of flicker)?

Parse errors that concern a range in a file.

Parse errors that concern a range in a file.

The previous token.

Scan the input to find the next token. Calls alexScanUser. This is the main lexing function where all the work happens. The function lexer, used by the parser is the continuation version of this function.

the previous token