Walk the commands tracking the section depth: an assumption outside any section is a file-wide axiom and is marked as an abstract function (see tokenizeCommand), while an assumption inside a section is a hypothesis the section abstracts over at its #end, so it keeps the parameter token type and only gains the abstract modifier.

A match branch: the constructor name is an enum member (as constructor uses are), the binders are parameters, the body is an ordinary term.

Highlight the fixed syntax of the language (command names, reserved words, operators) and holes directly from the lexer token stream.

This complements tokenizeModule, which highlights identifiers and special term formers from the parsed module. Fixed symbols do not need parsing at all: a := is a := wherever it occurs, and a hole ? (or ?name) is its own lexer token. Working on the token stream means that the grammar (and the abstract syntax) does not have to track positions of keywords, and that highlighting keeps working for files that (temporarily) fail to parse.

How to highlight a lexer token, if at all: fixed symbols by classifySymbol, holes as a distinct token. Identifiers are left to the AST pass (tokenizeModule), which knows their role.

How to highlight a fixed symbol of the grammar, if at all.

Combine tokens from the parsed module with tokens from the raw symbol stream. On overlap (same start position) the AST-based token wins, since it carries more precise semantics (e.g. unit as an enum member rather than a keyword). The result is sorted by position, as required for the LSP delta encoding.