# HG changeset patch
# User wenzelm
# Date 1727384641 -7200
# Node ID 980cc422526ecd7ca7cc24049b6178cee8bb10f7
# Parent  97924a26a5c3e80da3f7c17f9bf13239dc558363# Parent  cf96b584724df6ff1fa0a2d9b1d13512c8f56db9
merged

diff -r 97924a26a5c3 -r 980cc422526e src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Fri Aug 23 15:30:09 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy	Thu Sep 26 23:04:01 2024 +0200
@@ -30,29 +30,29 @@
   "_constify"           :: "id => ident"                        (\<open>_\<close>)
   "_constify"           :: "longid => ident"                    (\<open>_\<close>)
 
-  "_field_type"         :: "ident => type => field_type"        (\<open>(2_ ::/ _)\<close>)
+  "_field_type"         :: "ident => type => field_type"        (\<open>(\<open>indent=2 notation=\<open>infix field type\<close>\<close>_ ::/ _)\<close>)
   ""                    :: "field_type => field_types"          (\<open>_\<close>)
   "_field_types"        :: "field_type => field_types => field_types"    (\<open>_,/ _\<close>)
-  "_record_type"        :: "field_types => type"                (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
+  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
 
-  "_field"              :: "ident => 'a => field"               (\<open>(2_ =/ _)\<close>)
+  "_field"              :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
   ""                    :: "field => fields"                    (\<open>_\<close>)
   "_fields"             :: "field => fields => fields"          (\<open>_,/ _\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
+  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
 
-  "_field_update"       :: "ident => 'a => field_update"        (\<open>(2_ :=/ _)\<close>)
+  "_field_update"       :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
   ""                    :: "field_update => field_updates"      (\<open>_\<close>)
   "_field_updates"      :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
 
 no_syntax (ASCII)
-  "_record_type"        :: "field_types => type"                (\<open>(3'(| _ |'))\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(3'(| _,/ (2... ::/ _) |'))\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(3'(| _ |'))\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
+  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _ |'))\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (2... ::/ _) |'))\<close>)
+  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _ |'))\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (2... =/ _) |'))\<close>)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
 
 (* copied and adapted from Record.thy *)
 
diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Sep 26 23:04:01 2024 +0200
@@ -30,6 +30,7 @@
   val end_pos_of_token: token -> Position.T
   val is_proper: token -> bool
   val dummy: token
+  val is_dummy: token -> bool
   val literal: string -> token
   val is_literal: token -> bool
   val tokens_match_ord: token ord
@@ -40,8 +41,6 @@
   val terminals: string list
   val is_terminal: string -> bool
   val get_terminal: string -> token option
-  val suppress_literal_markup: string -> bool
-  val suppress_markup: token -> bool
   val literal_markup: string -> Markup.T list
   val reports_of_token: token -> Position.report list
   val reported_token_range: Proof.context -> token -> string
@@ -146,7 +145,9 @@
 
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
-val dummy = Token (token_kind_index Dummy, "", Position.no_range);
+val dummy_index = token_kind_index Dummy;
+val dummy = Token (dummy_index, "", Position.no_range);
+fun is_dummy tok = index_of_token tok = dummy_index;
 
 
 (* literals *)
@@ -199,9 +200,6 @@
 
 (* markup *)
 
-val suppress_literal_markup = Symbol.has_control_block o Symbol.explode;
-fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok);
-
 fun literal_markup s =
   let val syms = Symbol.explode s in
     if Symbol.has_control_block syms then []
diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu Sep 26 23:04:01 2024 +0200
@@ -14,8 +14,7 @@
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
-  exception PARSETREE of parsetree
-  val pretty_parsetree: parsetree -> Pretty.T
+  val pretty_parsetree: parsetree -> Pretty.T list
   val parse: gram -> string -> Lexicon.token list -> parsetree list
   val branching_level: int Config.T
 end;
@@ -32,6 +31,7 @@
 
 type tags = nt Symtab.table;
 val tags_empty: tags = Symtab.empty;
+fun tags_size (tags: tags) = Symtab.size tags;
 fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
 fun tags_lookup (tags: tags) = Symtab.lookup tags;
 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
@@ -88,9 +88,7 @@
 
 datatype gram =
   Gram of
-   {nt_count: int,
-    prod_count: int,
-    tags: tags,
+   {tags: tags,
     chains: chains,
     lambdas: nts,
     prods: nt_gram Vector.vector};
@@ -417,76 +415,75 @@
 
 val empty_gram =
   Gram
-   {nt_count = 0,
-    prod_count = 0,
-    tags = tags_empty,
+   {tags = tags_empty,
     chains = chains_empty,
     lambdas = nts_empty,
     prods = Vector.fromList [nt_gram_empty]};
 
-fun extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
-  let
-    (*Get tag for existing nonterminal or create a new one*)
-    fun get_tag nt_count tags nt =
-      (case tags_lookup tags nt of
-        SOME tag => (nt_count, tags, tag)
-      | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count));
+local
+
+fun make_tag s tags =
+  (case tags_lookup tags s of
+    SOME tag => (tag, tags)
+  | NONE =>
+      let val tag = tags_size tags
+      in (tag, tags_insert (s, tag) tags) end);
 
-    (*Convert symbols to the form used by the parser;
-      delimiters and predefined terms are stored as terminals,
-      nonterminals are converted to integer tags*)
-    fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
-      | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result =
-          symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result)
-      | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
+fun make_arg (s, p) tags =
+  (case Lexicon.get_terminal s of
+    NONE =>
+      let val (tag, tags') = make_tag s tags;
+      in (Nonterminal (tag, p), tags') end
+  | SOME tok => (Terminal tok, tags));
+
+fun extend_gram xprods gram =
+  let
+    fun make_symbs (Syntax_Ext.Delim s :: xsyms) tags =
+          let val (syms, tags') = make_symbs xsyms tags
+          in (Terminal (Lexicon.literal s) :: syms, tags') end
+      | make_symbs (Syntax_Ext.Argument a :: xsyms) tags =
           let
-            val (nt_count', tags', new_symb) =
-              (case Lexicon.get_terminal s of
-                NONE =>
-                  let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
-                  in (nt_count', tags', Nonterminal (s_tag, p)) end
-              | SOME tk => (nt_count, tags, Terminal tk));
-          in symb_of ss nt_count' tags' (new_symb :: result) end
-      | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result;
+            val (arg, tags') = make_arg a tags;
+            val (syms, tags'') = make_symbs xsyms tags';
+          in (arg :: syms, tags'') end
+      | make_symbs (_ :: xsyms) tags = make_symbs xsyms tags
+      | make_symbs [] tags = ([], tags);
 
-    (*Convert list of productions by invoking symb_of for each of them*)
-    fun prod_of [] nt_count prod_count tags result =
-          (nt_count, prod_count, tags, result)
-      | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
-            nt_count prod_count tags result =
-          let
-            val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
-            val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' [];
-          in
-            prod_of ps nt_count'' (prod_count + 1) tags''
-              ((lhs_tag, (prods, const, pri)) :: result)
-          end;
+    fun make_prod (Syntax_Ext.XProd (lhs, xsymbs, const, pri)) (result, tags) =
+      let
+        val (tag, tags') = make_tag lhs tags;
+        val (symbs, tags'') = make_symbs xsymbs tags';
+      in ((tag, (symbs, const, pri)) :: result, tags'') end;
 
-    val (nt_count', prod_count', tags', xprods') =
-      prod_of xprods nt_count prod_count tags [];
+
+    val Gram {tags, chains, lambdas, prods} = gram;
+
+    val (new_prods, tags') = fold make_prod xprods ([], tags);
 
     val array_prods' =
-      Array.tabulate (nt_count', fn i =>
-        if i < nt_count then Vector.nth prods i
+      Array.tabulate (tags_size tags', fn i =>
+        if i < Vector.length prods then Vector.nth prods i
         else nt_gram_empty);
 
     val (chains', lambdas') =
-      (chains, lambdas) |> fold (add_production array_prods') xprods';
+      (chains, lambdas) |> fold (add_production array_prods') new_prods;
   in
     Gram
-     {nt_count = nt_count',
-      prod_count = prod_count',
-      tags = tags',
+     {tags = tags',
       chains = chains',
       lambdas = lambdas',
       prods = Array.vector array_prods'}
   end;
 
+in
+
 fun make_gram [] _ (SOME gram) = gram
   | make_gram new_xprods _ (SOME gram) = extend_gram new_xprods gram
   | make_gram [] [] NONE = empty_gram
   | make_gram new_xprods old_xprods NONE = extend_gram (new_xprods @ old_xprods) empty_gram;
 
+end;
+
 
 
 (** parser **)
@@ -497,15 +494,11 @@
   Node of string * parsetree list |
   Tip of Lexicon.token;
 
-exception PARSETREE of parsetree;
-
-fun pretty_parsetree parsetree =
-  let
-    fun pretty (Node (c, pts)) =
-          [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))]
-      | pretty (Tip tok) =
-          if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
-  in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end;
+fun pretty_parsetree (Node (c, pts)) =
+      [Pretty.enclose "(" ")"
+        (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_parsetree pts))]
+  | pretty_parsetree (Tip tok) =
+      if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
 
 
 (* parser state *)
@@ -562,9 +555,6 @@
 
 fun movedot_nonterm tt (info, Nonterminal _ :: sa, ts) : state = (info, sa, tt @ ts);
 
-fun movedot_lambda p ((info, sa, ts): state) =
-  map_filter (fn (t, k) => if p <= k then SOME (info, sa, t @ ts) else NONE);
-
 
 (*trigger value for warnings*)
 val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
@@ -626,16 +616,21 @@
                   else (used, get_states A prec (Array.nth stateset j));
                 val States' = map (movedot_nonterm tt) Slist;
               in process used' (States' @ States) (S :: Si, Sii) end)
-  in process Inttab.empty states ([], []) end;
 
-fun produce gram stateset i input prev_token =
+    val (Si, Sii) = process Inttab.empty states ([], []);
+  in
+    Array.upd stateset i Si;
+    Array.upd stateset (i + 1) Sii
+  end;
+
+fun produce gram stateset i prev rest =
   (case Array.nth stateset i of
     [] =>
       let
-        val toks = if Lexicon.is_eof prev_token then input else prev_token :: input;
-        val pos = Position.here (Lexicon.pos_of_token prev_token);
+        val inp = if Lexicon.is_dummy prev then rest else prev :: rest;
+        val pos = Position.here (Lexicon.pos_of_token prev);
       in
-        if null toks then
+        if null inp then
           error ("Inner syntax error: unexpected end of input" ^ pos)
         else
           error ("Inner syntax error" ^ pos ^
@@ -645,18 +640,13 @@
                   Pretty.str "at", Pretty.brk 1,
                   Pretty.block
                    (Pretty.str "\"" ::
-                    Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
+                    Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last inp))) @
                     [Pretty.str "\""])])))
       end
   | states =>
-      (case input of
+      (case rest of
         [] => states
-      | c :: rest =>
-          let
-            val (Si, Sii) = process_states gram stateset i c states;
-            val _ = Array.upd stateset i Si;
-            val _ = Array.upd stateset (i + 1) Sii;
-          in produce gram stateset (i + 1) rest c end));
+      | c :: cs => (process_states gram stateset i c states; produce gram stateset (i + 1) c cs)));
 
 in
 
@@ -678,7 +668,7 @@
     val _ = Array.upd stateset 0 [S0];
 
     val pts =
-      produce gram stateset 0 input Lexicon.eof
+      produce gram stateset 0 Lexicon.dummy input
       |> map_filter (fn (_, _, [pt]) => SOME pt | _ => NONE);
   in if null pts then raise Fail "Inner syntax: no parse trees" else pts end;
 
diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu Sep 26 23:04:01 2024 +0200
@@ -68,7 +68,7 @@
 datatype symb =
   Arg of int |
   TypArg of int |
-  String of bool * string |
+  String of Markup.T list * string |
   Break of int |
   Block of Syntax_Ext.block * symb list;
 
@@ -131,41 +131,37 @@
 
 (* xprod_to_fmt *)
 
+fun make_string s = String ([], s);
+fun make_literal s = String (Lexicon.literal_markup s, s);
+
+fun make_arg (s, p) =
+  (if s = "type" then TypArg else Arg)
+  (if Lexicon.is_terminal s then 1000 else p);
+
 fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
   | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
       let
-        fun arg (s, p) =
-          (if s = "type" then TypArg else Arg)
-          (if Lexicon.is_terminal s then 1000 else p);
-
-        fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
-              apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
-                (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
-              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
-              apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.Bg block :: xsyms) =
+        fun make_symbs (Syntax_Ext.Delim s :: xsyms) = make_symbs xsyms |>> cons (make_literal s)
+          | make_symbs (Syntax_Ext.Argument a :: xsyms) = make_symbs xsyms |>> cons (make_arg a)
+          | make_symbs (Syntax_Ext.Space s :: xsyms) = make_symbs xsyms |>> cons (make_string s)
+          | make_symbs (Syntax_Ext.Bg block :: xsyms) =
               let
-                val (bsyms, xsyms') = xsyms_to_syms xsyms;
-                val (syms, xsyms'') = xsyms_to_syms xsyms';
-              in
-                (Block (block, bsyms) :: syms, xsyms'')
-              end
-          | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
-              apfst (cons (Break i)) (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
-          | xsyms_to_syms [] = ([], []);
+                val (bsyms, xsyms') = make_symbs xsyms;
+                val (syms, xsyms'') = make_symbs xsyms';
+              in (Block (block, bsyms) :: syms, xsyms'') end
+          | make_symbs (Syntax_Ext.Brk i :: xsyms) = make_symbs xsyms |>> cons (Break i)
+          | make_symbs (Syntax_Ext.En :: xsyms) = ([], xsyms)
+          | make_symbs [] = ([], []);
 
-        fun nargs (Arg _ :: syms) = nargs syms + 1
-          | nargs (TypArg _ :: syms) = nargs syms + 1
-          | nargs (String _ :: syms) = nargs syms
-          | nargs (Break _ :: syms) = nargs syms
-          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
-          | nargs [] = 0;
+        fun count_args (Arg _ :: syms) = Integer.add 1 #> count_args syms
+          | count_args (TypArg _ :: syms) = Integer.add 1 #> count_args syms
+          | count_args (String _ :: syms) = count_args syms
+          | count_args (Break _ :: syms) = count_args syms
+          | count_args (Block (_, bsyms) :: syms) = count_args syms #> count_args bsyms
+          | count_args [] = I;
       in
-        (case xsyms_to_syms xsymbs of
-          (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
+        (case make_symbs xsymbs of
+          (symbs, []) => SOME (const, (symbs, count_args symbs 0, pri))
         | _ => raise Fail "Unbalanced pretty-printing blocks")
       end;
 
@@ -207,6 +203,14 @@
 val pretty_curried = Config.declare_bool ("Syntax.pretty_curried", \<^here>) (K false);
 val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
 
+local
+
+val par_block = Syntax_Ext.block_indent 1;
+val par_bg = make_literal "(";
+val par_en = make_literal ")";
+
+in
+
 fun pretty ctxt tabs trf markup_trans markup_extern ast0 =
   let
     val type_mode = Config.get ctxt pretty_type_mode;
@@ -234,13 +238,10 @@
                 |> Config.put pretty_priority p
               in (pretty ctxt' tabs trf markup_trans markup_extern t @ Ts, args') end
           end
-      | synT m (String (do_mark, s) :: symbs, args) =
+      | synT m (String (literal_markup, s) :: symbs, args) =
           let
             val (Ts, args') = synT m (symbs, args);
-            val T =
-              if do_mark
-              then Pretty.marks_str (m @ Lexicon.literal_markup s, s)
-              else Pretty.str s;
+            val T = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
           in (T :: Ts, args') end
       | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
           let
@@ -256,10 +257,9 @@
             val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
           in (T :: Ts, args') end
 
-    and parT m (pr, args, p, p': int) = #1 (synT m
-          (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
-            [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
-           else pr, args))
+    and parT m (pr, args, p, p') = #1 (synT m
+          (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
+           then [Block (par_block, par_bg :: pr @ [par_en])] else pr, args))
 
     and atomT a = Pretty.marks_str (#1 markup_extern a, #2 markup_extern a)
 
@@ -295,6 +295,8 @@
       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
   in astT (ast0, Config.get ctxt pretty_priority) end;
 
+end;
+
 
 (* pretty_term_ast *)
 
diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Sep 26 23:04:01 2024 +0200
@@ -158,8 +158,8 @@
     val append_reports = Position.append_reports reports;
 
     fun report_pos tok =
-      if Lexicon.suppress_markup tok then Position.none
-      else Lexicon.pos_of_token tok;
+      if Lexicon.is_literal tok andalso null (Lexicon.literal_markup (Lexicon.str_of_token tok))
+      then Position.none else Lexicon.pos_of_token tok;
 
     fun trans a args =
       (case trf a of
@@ -358,8 +358,7 @@
           (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^
             " produces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
-              (take limit pts))];
+            map (Pretty.string_of o Pretty.item o Parser.pretty_parsetree) (take limit pts))];
 
   in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
 
diff -r 97924a26a5c3 -r 980cc422526e src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Fri Aug 23 15:30:09 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Thu Sep 26 23:04:01 2024 +0200
@@ -196,7 +196,7 @@
 syntax
   "" :: "i \<Rightarrow> tuple_args"  (\<open>_\<close>)
   "_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args"  (\<open>_,/ _\<close>)
-  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(_,/ _)\<rangle>\<close>)
+  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(\<open>notation=\<open>mixfix tuple\<close>\<close>_,/ _)\<rangle>\<close>)
 syntax_consts
   "_Tuple_args" "_Tuple" == Pair
 translations