From 63e4fa476e2f9180dd3dc630a5fc937abf849860 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 12:17:20 +0100 Subject: [PATCH 01/10] Accept cartouche RHS in type_synonym declarations `type_synonym name = \...\` (cartouche-delimited inner syntax, as opposed to a "..." string) failed to parse: the type_synonym rule only allowed `ID | QUOTED_STRING` on the right of `=`, while every other inner-syntax position already routes through `embedded`, which accepts cartouches. Add `cartouche` to the alternatives. 43 AFP thy files use this form. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 816fd25..15c2c1e 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2193,7 +2193,7 @@ ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" typedecl : "typedecl" typespec mixfix? -type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | QUOTED_STRING) mixfix? +type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | QUOTED_STRING | cartouche) mixfix? # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.13 diff --git a/tests/test_parser.py b/tests/test_parser.py index 06e38a9..1f0f8d5 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -264,6 +264,12 @@ "theory T imports Main begin\ntype_synonym 'a mylist = \"'a list\"\nend", True, ), + ( + "type_synonym_cartouche", + "theory T imports Main begin\n" + "type_synonym int_poly = \\int mpoly\\\nend", + True, + ), # ----------------------------------------------------------------------- # Constant declarations # ----------------------------------------------------------------------- From 7d5da0b8b003a1e305bde27799b8bf3ac20f3e85 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 13:55:24 +0100 Subject: [PATCH 02/10] Accept private/qualified modifiers on top-level commands `private` and `qualified` are local-theory command modifiers. The `local_theory` rule (block bodies of context/locale/instantiation) already allowed them, but the top-level `theory` rule did not, so a bare `qualified definition ...` / `private lemma ...` directly under `theory ... begin` failed to parse. Mirror the optional `("private" | "qualified")?` prefix onto the top-level goal/statement alternatives. 328 AFP thy files use these modifiers (qualified is standard in HOL/Library at the global theory level). Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 4 ++-- tests/test_parser.py | 11 +++++++++++ 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 15c2c1e..6190673 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1594,8 +1594,8 @@ context: ( print_locale | print_locales | print_state )* -theory: ( goal proof_prove - | statement +theory: ( ("private" | "qualified")? goal proof_prove + | ("private" | "qualified")? statement | class_instance proof_prove | derive )* diff --git a/tests/test_parser.py b/tests/test_parser.py index 1f0f8d5..92d7e62 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -270,6 +270,17 @@ "type_synonym int_poly = \\int mpoly\\\nend", True, ), + ( + "qualified_toplevel_definition", + "theory T imports Main begin\n" + 'qualified definition bar :: nat where "bar = 0"\nend', + True, + ), + ( + "private_toplevel_lemma", + 'theory T imports Main begin\nprivate lemma l: "x = x" by simp\nend', + True, + ), # ----------------------------------------------------------------------- # Constant declarations # ----------------------------------------------------------------------- From f30312b1259cb6081920516a5d9f6b7f2428d8b8 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 14:16:42 +0100 Subject: [PATCH 03/10] Accept \<^sub> subscripts in type variables and typespec names TYPE_IDENT only matched plain/Greek type variables (`'a`, `'\`), not subscripted ones (`'a\<^sub>h`), even though inner-syntax type positions already accept them. As a result `datatype`/`type_synonym`/ `typedecl` declarations whose type arguments or constructor names carry `\<^sub>` subscripts failed to parse (e.g. AFP's ADS_Construction: `datatype 'a\<^sub>h blindable\<^sub>h = ...`). Extend the TYPE_IDENT terminal with a `\<^sub>...` segment (ordered first in the repeat group so the empty-matching alternative doesn't pre-empt it). Also allow a bare TYPE_IDENT on the type_synonym RHS (`type_synonym 'a foo = 'a`). Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 4 ++-- tests/test_parser.py | 20 ++++++++++++++++++++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6190673..b964a2d 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1574,7 +1574,7 @@ TERM_VAR: /\?[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ TYPE_VAR: /'[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ // Other predefined tokens -TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(_?\d*[a-zA-Z_\']*)*/ +TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(\\<\^sub>[a-zA-Z0-9_\']*|_?\d*[a-zA-Z_\']*)*/ SUBSCRIPT: "\\<^sub>" @@ -2193,7 +2193,7 @@ ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" typedecl : "typedecl" typespec mixfix? -type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | QUOTED_STRING | cartouche) mixfix? +type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | TYPE_IDENT | QUOTED_STRING | cartouche) mixfix? # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.13 diff --git a/tests/test_parser.py b/tests/test_parser.py index 92d7e62..6a11e86 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -270,6 +270,19 @@ "type_synonym int_poly = \\int mpoly\\\nend", True, ), + ( + "type_synonym_subscripted_type_vars", + "theory T imports Main begin\n" + "type_synonym ('a\\<^sub>h, 'b\\<^sub>h) sum\\<^sub>h = " + '"\'a\\<^sub>h + \'b\\<^sub>h"\nend', + True, + ), + ( + "type_synonym_type_var_rhs", + "theory T imports Main begin\n" + "type_synonym 'a blindable = 'a\nend", + True, + ), ( "qualified_toplevel_definition", "theory T imports Main begin\n" @@ -878,6 +891,13 @@ "end", True, ), + ( + "datatype_subscripted_type_var_and_constructor", + "theory T imports Main begin\n" + "datatype 'a\\<^sub>h blindable\\<^sub>h = Content 'a\\<^sub>h\n" + "end", + True, + ), # ----------------------------------------------------------------------- # datatype BNF type-argument annotations (dead / selectors) # ----------------------------------------------------------------------- From ac4e7af434056fe8b08bba2d29726bff04234e1a Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 14:20:20 +0100 Subject: [PATCH 04/10] Accept repeated and symbol subscripts in identifier names The `name` terminal allowed at most one `\<^sub>X` segment per identifier and its standalone-subscript alternative had a stray backslash (so it never matched). Identifiers with multiple subscripts (`Seq\<^sub>p\<^sub>t\<^sub>i`, `lang\<^sub>M\<^sub>2\<^sub>L`) or a symbol after the subscript marker (`\\<^sub>\`) therefore truncated mid-name, failing every command that names such an entity (definition, lemmas, abbreviation, interpretation, ...). Make the subscript segment repeatable (`?` -> `*`) and fix the standalone `\<^sub>` alternative so subscripts can chain into following Greek/symbol glyphs. 142 AFP files use multi-subscript command names; 773 use a subscript-then-symbol identifier somewhere. Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index b964a2d..edffe68 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1715,7 +1715,7 @@ name: QUOTED_STRING | /[+]+/ | SYM_IDENT // | (ID | GREEK | SUBSCRIPT | "." | "_" | NAT | "'" | letter)+ - | /(([a-zA-Z_][a-zA-Z_0-9\']*(\\<\^sub>[a-zA-Z0-9_]*)?)|(\\<((alpha)|(beta)|(gamma)|(delta)|(epsilon)|(zeta)|(eta)|(theta)|(iota)|(kappa)|(mu)|(nu)|(xi)|(pi)|(rho)|(sigma)|(tau)|(upsilon)|(phi)|(chi)|(psi)|(omega)|(Gamma)|(Delta)|(Theta)|(Lambda)|(Xi)|(Pi)|(Sigma)|(Upsilon)|(Phi)|(Psi)|(Omega))>)|(\\<\\^sub>)|([._'])|([0-9])|([a-zA-Z]+)|(\\?<[a-zA-Z]+>))+/ + | /(([a-zA-Z_][a-zA-Z_0-9\']*(\\<\^sub>[a-zA-Z0-9_]*)*)|(\\<((alpha)|(beta)|(gamma)|(delta)|(epsilon)|(zeta)|(eta)|(theta)|(iota)|(kappa)|(mu)|(nu)|(xi)|(pi)|(rho)|(sigma)|(tau)|(upsilon)|(phi)|(chi)|(psi)|(omega)|(Gamma)|(Delta)|(Theta)|(Lambda)|(Xi)|(Pi)|(Sigma)|(Upsilon)|(Phi)|(Psi)|(Omega))>)|(\\<\^sub>)|([._'])|([0-9])|([a-zA-Z]+)|(\\?<[a-zA-Z]+>))+/ | "\\" par_name: "(" name ")" diff --git a/tests/test_parser.py b/tests/test_parser.py index 6a11e86..54ea720 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -860,6 +860,22 @@ True, ), # ----------------------------------------------------------------------- + # identifiers with repeated / symbol subscripts in name position + # ----------------------------------------------------------------------- + ( + "definition_repeated_subscript_name", + "theory T imports Main begin\n" + "definition lang\\<^sub>M\\<^sub>2\\<^sub>L :: nat where " + '"lang\\<^sub>M\\<^sub>2\\<^sub>L = 0"\nend', + True, + ), + ( + "lemmas_greek_symbol_subscript_name", + "theory T imports Main begin\n" + "lemmas \\\\<^sub>\\_cong = foo\nend", + True, + ), + # ----------------------------------------------------------------------- # class with multiple superclasses # ----------------------------------------------------------------------- ( From a176417dd0024f688c45fe5b193360cf21c3936d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 14:22:35 +0100 Subject: [PATCH 05/10] Accept qualified class names in sort/arity positions `sort` only allowed a bare ID or quoted string, so a qualified class name (`heap.rep`) in an arity failed: `instance unit :: heap.rep ..`. Add the existing LONG_IDENT terminal (dotted identifier) as a sort alternative, which also covers qualified classes anywhere a sort is accepted. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index edffe68..506d882 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1796,7 +1796,7 @@ typespec_sorts: typeargs_sorts? name # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 3.3.6 # -sort: ID | QUOTED_STRING +sort: ID | LONG_IDENT | QUOTED_STRING sort_list_comma_sep: sort ("," sort)* diff --git a/tests/test_parser.py b/tests/test_parser.py index 54ea720..a8bcdea 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -639,6 +639,11 @@ "end", True, ), + ( + "instance_qualified_class_name", + "theory T imports Main begin\ninstance unit :: heap.rep ..\nend", + True, + ), # ----------------------------------------------------------------------- # abbreviation with an (output) print mode # ----------------------------------------------------------------------- From 2a2f14c62e65dc2c3ef1a18ef34f8f10105970b2 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 14:59:19 +0100 Subject: [PATCH 06/10] Accept (in -) target, ctor discriminators, qualified attribute args MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three independent gaps found by statement-level localization: - `(in -)` local-theory target (global scope) on definition/abbreviation/ etc. — the target rule only allowed `(in name)`. ~94 AFP files. - datatype constructor discriminators: `datatype t = is_PUSH: PUSH | ...` — a constructor may carry a leading `discr:` name. Added the optional `(name ":")?` prefix to both constructor alternatives. - qualified fact names as attribute arguments: `[simplified bar.inject]`, `[OF foo.bar]` — the `arg` rule accepted ID but not LONG_IDENT, so a dotted fact reference inside `[...]` failed. Very common (~960 files use a dotted name inside an attribute bracket). Adds regression tests for each. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 7 ++++--- tests/test_parser.py | 18 ++++++++++++++++++ 2 files changed, 22 insertions(+), 3 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 506d882..e1bab4d 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1879,6 +1879,7 @@ attribute: "OF" thms args: arg* arg: ID + | LONG_IDENT | cartouche | "False" | "for" @@ -2030,7 +2031,7 @@ thy_bounds: name | ("(" name ("|" name)* ")") locale_theory_context: "context" comment_block? name opening? "begin" local_theory "end" | "context" comment_block? includes? context_elem* "begin" local_theory "end" -local_theory_target: "(" "in" name ")" +local_theory_target: "(" "in" (name | "-") ")" # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.3 @@ -2624,8 +2625,8 @@ generic_type : (type | ("(" type ("," type)*")")) name? constructors : constructor ("|" constructor)* -constructor : comment_block? ID TYPE_IDENT mixfix? comment_block? - | comment_block? ( name +constructor : comment_block? (name ":")? ID TYPE_IDENT mixfix? comment_block? + | comment_block? (name ":")? ( name | cartouche | ("(" (cartouche | (name ":" name) | (name ":" QUOTED_STRING)) ")") )+ mixfix? comment_block? diff --git a/tests/test_parser.py b/tests/test_parser.py index a8bcdea..dce5206 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -644,6 +644,18 @@ "theory T imports Main begin\ninstance unit :: heap.rep ..\nend", True, ), + ( + "definition_global_target_dash", + "theory T imports Main begin\n" + 'definition (in -) foo :: nat where "foo = 0"\nend', + True, + ), + ( + "inductive_cases_qualified_attribute_arg", + "theory T imports Main begin\n" + 'inductive_cases fooCases[simplified bar.inject]: "P x"\nend', + True, + ), # ----------------------------------------------------------------------- # abbreviation with an (output) print mode # ----------------------------------------------------------------------- @@ -905,6 +917,12 @@ "theory T imports Main begin\ndatatype ('a::type) box = Box 'a\nend", True, ), + ( + "datatype_constructor_discriminators", + "theory T imports Main begin\n" + "datatype pr_op = is_PUSH: PUSH | is_RELABEL: RELABEL\nend", + True, + ), ( "datatype_multi_sort_annotated_tvars", "theory T imports Main begin\n" From bb41243b2f0872c9928e90404ac135186abb7481 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 16:42:56 +0100 Subject: [PATCH 07/10] Accept custom print-mode names in mode annotations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `mode` rule only allowed the literal modes `input`/`output`/`ASCII` inside parentheses, so a custom print mode — `abbreviation (latex) ...`, `notation (do_notation) ...`, the modal-logic `(uniA_i)` modes — failed. Add the general `"(" name ")"` form. ~104 AFP files use a custom print mode on abbreviation/notation. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 1 + tests/test_parser.py | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index e1bab4d..8819b45 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2554,6 +2554,7 @@ mode: ID | "(" "input" ")" | "(" "output" ")" | "(" "ASCII" ")" + | "(" name ")" # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 8.5.2 diff --git a/tests/test_parser.py b/tests/test_parser.py index dce5206..87b0b08 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -666,6 +666,13 @@ "end", True, ), + ( + "abbreviation_custom_print_mode", + "theory T imports Main begin\n" + 'abbreviation (latex) foo where "foo = x"\n' + "end", + True, + ), # ----------------------------------------------------------------------- # inductive_simps command # ----------------------------------------------------------------------- From 5b01c3f6552367fd3fd288785858b82e3f549225 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 16:44:36 +0100 Subject: [PATCH 08/10] Accept qualified type names on the type_synonym RHS `type_synonym error = String.literal` (and other `A.b` qualified type names) failed: the RHS allowed ID/TYPE_IDENT/QUOTED_STRING/cartouche but not LONG_IDENT. Add it. ~21 AFP files. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 8819b45..962f182 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2194,7 +2194,7 @@ ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" typedecl : "typedecl" typespec mixfix? -type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | TYPE_IDENT | QUOTED_STRING | cartouche) mixfix? +type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | LONG_IDENT | TYPE_IDENT | QUOTED_STRING | cartouche) mixfix? # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.13 diff --git a/tests/test_parser.py b/tests/test_parser.py index 87b0b08..d675700 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -283,6 +283,12 @@ "type_synonym 'a blindable = 'a\nend", True, ), + ( + "type_synonym_qualified_rhs", + "theory T imports Main begin\n" + "type_synonym error = String.literal\nend", + True, + ), ( "qualified_toplevel_definition", "theory T imports Main begin\n" From a00d27e7a8951c93d12f6b0979eea823c20cd632 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 17:03:10 +0100 Subject: [PATCH 09/10] Accept legacy {* ... *} verbatim markup in document and ML blocks MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pre-2016 Isabelle used {* ... *} (rather than cartouches) for document text and ML/source bodies. Neither parsed: section/subsection/text/etc. accepted only cartouche/string/ID, and the ML/setup/local_setup rule only cartouche/name/string. Add a VERBATIM_TEXT terminal (/\{\*...\*\}/, non-greedy) and wire it into doc_block and the ml rule. Deliberately NOT added to the hot `embedded` rule (rare legacy method_setup bodies aren't worth the Earley breadth). ~66 AFP files use {* — 22 in doc commands, ~56 in ML/ML_val/setup blocks. Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 7 +++++-- tests/test_parser.py | 13 +++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 962f182..9fac9d6 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -7,6 +7,9 @@ QUOTED_STRING: "\"" /[\s\S]*?/ "\"" | "`" /[\s\S]*?/ "`" +// Legacy (pre-2016) verbatim document/source text: {* ... *} +VERBATIM_TEXT: /\{\*[\s\S]*?\*\}/ + // Tokens for cartouche CARTOUCHE_OPEN: "\\" CARTOUCHE_TEXT: /[^\\]+/ @@ -1946,7 +1949,7 @@ doc_block: ( "chapter" | "text" | "text_raw" | "txt" - | COMMENT_CARTOUCHE) ("(" "in" name ")")? (cartouche | QUOTED_STRING | ID) + | COMMENT_CARTOUCHE) ("(" "in" name ")")? (cartouche | QUOTED_STRING | VERBATIM_TEXT | ID) comment_block: COMMENT_CARTOUCHE cartouche @@ -2186,7 +2189,7 @@ spec: name ("\\" | "==") term ("(" "unchecked" ")")? # ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" - | "SML_file" | "setup" | "local_setup" ) (name | cartouche | QUOTED_STRING) + | "SML_file" | "setup" | "local_setup" ) (name | cartouche | VERBATIM_TEXT | QUOTED_STRING) # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.12.2 diff --git a/tests/test_parser.py b/tests/test_parser.py index d675700..70c8b6f 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -679,6 +679,19 @@ "end", True, ), + ( + "legacy_verbatim_doc_markup", + "theory T imports Main begin\n" + "subsubsection {* Monotonicity *}\n" + "text {* some legacy text *}\nend", + True, + ), + ( + "legacy_verbatim_ml_block", + "theory T imports Main begin\n" + "ML {* val x = 1; fun f y = y + x *}\nend", + True, + ), # ----------------------------------------------------------------------- # inductive_simps command # ----------------------------------------------------------------------- From acf3bd814e089299b6cc089e06f17b25377f265d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 17:23:51 +0100 Subject: [PATCH 10/10] Apply ruff format to test additions CI `ruff format --check` flagged the new test cases. No semantic change. Co-Authored-By: Claude Opus 4.8 (1M context) --- tests/test_parser.py | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/tests/test_parser.py b/tests/test_parser.py index 70c8b6f..6043582 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -274,19 +274,17 @@ "type_synonym_subscripted_type_vars", "theory T imports Main begin\n" "type_synonym ('a\\<^sub>h, 'b\\<^sub>h) sum\\<^sub>h = " - '"\'a\\<^sub>h + \'b\\<^sub>h"\nend', + "\"'a\\<^sub>h + 'b\\<^sub>h\"\nend", True, ), ( "type_synonym_type_var_rhs", - "theory T imports Main begin\n" - "type_synonym 'a blindable = 'a\nend", + "theory T imports Main begin\ntype_synonym 'a blindable = 'a\nend", True, ), ( "type_synonym_qualified_rhs", - "theory T imports Main begin\n" - "type_synonym error = String.literal\nend", + "theory T imports Main begin\ntype_synonym error = String.literal\nend", True, ), ( @@ -688,8 +686,7 @@ ), ( "legacy_verbatim_ml_block", - "theory T imports Main begin\n" - "ML {* val x = 1; fun f y = y + x *}\nend", + "theory T imports Main begin\nML {* val x = 1; fun f y = y + x *}\nend", True, ), # -----------------------------------------------------------------------