Email Gateway (Jun 11 2026 at 07:10): Email Gateway (Jun 11 2026 at 07:10):From: "w.sun" <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
When porting Isabelle's span tokenizer to a Python PIDE client, I found that
the Scala and ML implementations decide "is this token a command modifier?"
in two different ways. Scala consults the keyword table; ML hardcodes the
literals private/qualified. The two agree today only because those are the
only before_command keywords declared anywhere in the 2025 sources — but the
ML side would silently ignore any new before_command keyword a theory
declares, whereas the Scala side would honor it.
Scala — table-driven (src/Pure/Isar/keyword.scala:203):
def is_before_command(token: Token): Boolean =
token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
Outer_Syntax.parse_spans uses this predicate to start a new span
(src/Pure/Isar/outer_syntax.scala:191).
ML — hardcoded literals (src/Pure/Isar/token.ML:254):
val is_command_modifier =
keyword_with (fn x => x = "private" orelse x = "qualified");
Outer_Syntax.parse_spans uses this to start a new span
(src/Pure/Isar/outer_syntax.ML:197):
else if Token.is_command_modifier tok orelse
Token.is_command tok andalso
(not (exists Token.is_command_modifier content) orelse exists
Token.is_command content)
then (flush (result, content, ignored), [tok], [])
A theory header such as
keywords "foo" :: before_command
would make foo a span-flushing modifier under the Scala tokenizer (jEdit,
batch dependency analysis) but not under the ML prover's own
Outer_Syntax.parse_spans. The span boundaries the two produce would diverge
for that theory.
Is the hardcoding in token.ML:254 intentional (e.g. before_command is
considered a closed, Pure-only concept by design), or should the ML side carry
the before_command marking through Keyword.keywords the way Scala's
kinds map does?
Last updated: Jun 12 2026 at 04:13 UTC