# HG changeset patch
# User paulson
# Date 1725011088 -3600
# Node ID f38e59e1c019ac3ba54e95a55341d2cff55a2680
# Parent  bcecb69f72faaac2dc4dbea8b09eb19f3b90988d# Parent  07c51801c2ea35a55161a004e50a1eff7fb2140b
merged

diff -r 07c51801c2ea -r f38e59e1c019 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -453,7 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 
-    syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
+    syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]")
 
 text \<open>\blankline\<close>
 
diff -r 07c51801c2ea -r f38e59e1c019 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -79,13 +79,16 @@
 
 (*<*)
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
 syntax
-  "_MTuple"      :: "['a, args] \<Rightarrow> 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple"     == MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
-  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
-  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition keysFor :: "msg set \<Rightarrow> key set" where
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -49,10 +49,13 @@
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
 syntax
-  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple" \<rightleftharpoons> MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -23,8 +23,13 @@
 code_lazy_type llist
 
 no_notation lazy_llist ("_")
-syntax "_llist" :: "args => 'a list"    ("\<^bold>[(_)\<^bold>]")
-syntax_consts "_llist" == lazy_llist
+nonterminal llist_args
+syntax
+  "" :: "'a \<Rightarrow> llist_args"  ("_")
+  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
+  "_llist" :: "llist_args => 'a list"    ("\<^bold>[(_)\<^bold>]")
+syntax_consts
+  "_llist_args" "_llist" == lazy_llist
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -348,7 +348,13 @@
 
 subsection \<open>List-style syntax for polynomials\<close>
 
-syntax "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
+nonterminal poly_args
+syntax
+  "" :: "'a \<Rightarrow> poly_args"  ("_")
+  "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args"  ("_,/ _")
+  "_poly" :: "poly_args \<Rightarrow> 'a poly"  ("[:(_):]")
+syntax_consts
+  "_poly_args" "_poly" \<rightleftharpoons> pCons
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -178,12 +178,13 @@
     (infixl "\<union>\<natural>" 65) where
   "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
+nonterminal convex_pd_args
 syntax
-  "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
-
+  "" :: "logic \<Rightarrow> convex_pd_args"  ("_")
+  "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args"  ("_,/ _")
+  "_convex_pd" :: "convex_pd_args \<Rightarrow> logic"  ("{_}\<natural>")
 syntax_consts
-  "_convex_pd" == convex_add
-
+  "_convex_pd_args" "_convex_pd" == convex_add
 translations
   "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -69,9 +69,12 @@
 
 subsection \<open>List enumeration\<close>
 
+nonterminal llist_args
 syntax
-  "_totlist" :: "args \<Rightarrow> 'a Seq"  ("[(_)!]")
-  "_partlist" :: "args \<Rightarrow> 'a Seq"  ("[(_)?]")
+  "" :: "'a \<Rightarrow> llist_args"  ("_")
+  "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
+  "_totlist" :: "llist_args \<Rightarrow> 'a Seq"  ("[(_)!]")
+  "_partlist" :: "llist_args \<Rightarrow> 'a Seq"  ("[(_)?]")
 syntax_consts
   "_totlist" "_partlist" \<rightleftharpoons> Consq
 translations
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -133,12 +133,13 @@
     (infixl "\<union>\<flat>" 65) where
   "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
+nonterminal lower_pd_args
 syntax
-  "_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
-
+  "" :: "logic \<Rightarrow> lower_pd_args"  ("_")
+  "_lower_pd_args" :: "logic \<Rightarrow> lower_pd_args \<Rightarrow> lower_pd_args"  ("_,/ _")
+  "_lower_pd" :: "lower_pd_args \<Rightarrow> logic" ("{_}\<flat>")
 syntax_consts
-  "_lower_pd" == lower_add
-
+  "_lower_pd_args" "_lower_pd" == lower_add
 translations
   "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/HOLCF/Sprod.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -40,8 +40,13 @@
 definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
   where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
-syntax "_stuple" :: "[logic, args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
-syntax_consts "_stuple" \<rightleftharpoons> spair
+nonterminal stuple_args
+syntax
+  "" :: "logic \<Rightarrow> stuple_args"  ("_")
+  "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args"  ("_,/ _")
+  "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
+syntax_consts
+  "_stuple_args" "_stuple" \<rightleftharpoons> spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -131,12 +131,13 @@
     (infixl "\<union>\<sharp>" 65) where
   "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
+nonterminal upper_pd_args
 syntax
-  "_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
-
+  "" :: "logic \<Rightarrow> upper_pd_args"  ("_")
+  "_upper_pd_args" :: "logic \<Rightarrow> upper_pd_args \<Rightarrow> upper_pd_args"  ("_,/ _")
+  "_upper_pd" :: "upper_pd_args \<Rightarrow> logic"  ("{_}\<sharp>")
 syntax_consts
-  "_upper_pd" == upper_add
-
+  "_upper_pd_args" "_upper_pd" == upper_add
 translations
   "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
   "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -164,12 +164,13 @@
 lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
   by simp
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == finsert
-
+  "_fset_args" "_fset" == finsert
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -47,8 +47,7 @@
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
 
 syntax_consts
-  "_do_block" "_do_cons" \<rightleftharpoons> bind_do and
-  "_do_bind" "_thenM" \<rightleftharpoons> bind and
+  "_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and
   "_do_let" \<rightleftharpoons> Let
 
 translations
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -91,10 +91,13 @@
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
 by (rule add_mset_in_multiset)
 
+nonterminal multiset_args
 syntax
-  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
+  "" :: "'a \<Rightarrow> multiset_args"  ("_")
+  "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args"  ("_,/ _")
+  "_multiset" :: "multiset_args \<Rightarrow> 'a multiset"    ("{#(_)#}")
 syntax_consts
-  "_multiset" == add_mset
+  "_multiset_args" "_multiset" == add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Library/Open_State_Syntax.thy
--- a/src/HOL/Library/Open_State_Syntax.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Library/Open_State_Syntax.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -119,6 +119,8 @@
 
 nonterminal sdo_binds and sdo_bind
 
+definition "sdo_syntax = ()"
+
 syntax
   "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
   "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
@@ -130,6 +132,11 @@
 syntax (ASCII)
   "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
 
+syntax_consts
+  "_sdo_block" "_sdo_cons" == sdo_syntax and
+  "_sdo_bind" == scomp and
+  "_sdo_let" == Let
+
 translations
   "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
     == "CONST scomp t (\<lambda>p. e)"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/List.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -42,13 +42,16 @@
 
 lemmas set_simps = list.set (* legacy *)
 
+
+text \<open>List enumeration\<close>
+
+nonterminal list_args
 syntax
-  \<comment> \<open>list Enumeration\<close>
-  "_list" :: "args => 'a list"    ("[(_)]")
-
+  "" :: "'a \<Rightarrow> list_args"  ("_")
+  "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args"  ("_,/ _")
+  "_list" :: "list_args => 'a list"    ("[(_)]")
 syntax_consts
-  "_list" == Cons
-
+  "_list_args" "_list" == Cons
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -48,13 +48,16 @@
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple"     == MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
-  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
-  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Prolog/Test.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -16,13 +16,18 @@
   Nil   :: "'a list"                                  ("[]")
   Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
 
-syntax
-  (* list Enumeration *)
-  "_list"     :: "args => 'a list"                          ("[(_)]")
+text \<open>List enumeration\<close>
 
+nonterminal list_args
+syntax
+  "" :: "'a \<Rightarrow> list_args"  ("_")
+  "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args"  ("_,/ _")
+  "_list" :: "list_args => 'a list"    ("[(_)]")
+syntax_consts
+  "_list_args" "_list" == Cons
 translations
-  "[x, xs]"     == "x#[xs]"
-  "[x]"         == "x#[]"
+  "[x, xs]" == "x#[xs]"
+  "[x]" == "x#[]"
 
 typedecl person
 
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -95,12 +95,13 @@
 
 end
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == fcons
-
+  "_fset_args" "_fset" == fcons
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -288,12 +288,13 @@
   "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "Cons" by auto
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == insert_fset
-
+  "_fset_args" "_fset" == insert_fset
 translations
   "{|x, xs|}" == "CONST insert_fset x {|xs|}"
   "{|x|}"     == "CONST insert_fset x {||}"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -68,10 +68,13 @@
 
 
 (*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
+nonterminal mtuple_args
 syntax
-  "_MTuple"      :: "['a, args] \<Rightarrow> 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple"     == MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
   "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/Set.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -143,10 +143,13 @@
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
+nonterminal finset_args
 syntax
-  "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")
+  "" :: "'a \<Rightarrow> finset_args"  ("_")
+  "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args"  ("_,/ _")
+  "_Finset" :: "finset_args \<Rightarrow> 'a set"    ("{(_)}")
 syntax_consts
-  "_Finset" \<rightleftharpoons> insert
+  "_Finset_args" "_Finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
diff -r 07c51801c2ea -r f38e59e1c019 src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -39,8 +39,13 @@
   = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
 
-syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
-syntax_consts "_llist" == LCons
+nonterminal llist_args
+syntax
+  "" :: "'a \<Rightarrow> llist_args"  ("_")
+  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
+  "_llist" :: "llist_args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+syntax_consts
+  "_llist_args" "_llist" == LCons
 translations
   "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
   "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
diff -r 07c51801c2ea -r f38e59e1c019 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Pure/Build/build_manager.scala	Fri Aug 30 10:44:48 2024 +0100
@@ -802,22 +802,27 @@
           result_futures + (context.name -> result_future))
       }
 
-      def running: List[String] = process_futures.keys.toList
+      def running: List[String] = process_futures.keys.toList.filterNot(cancelling_until.contains)
+
+      private def maybe_result(name: String): Option[Process_Result] =
+        for (future <- result_futures.get(name) if future.is_finished) yield
+          future.join_result match {
+            case Exn.Res(result) => result
+            case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
+          }
 
       private def do_terminate(name: String): Boolean = {
-        val is_late = cancelling_until(name) > Time.now()
+        val is_late = Time.now() > cancelling_until(name)
         if (is_late) process_futures(name).join.terminate()
         is_late
       }
 
       def update: (State, Map[String, Process_Result]) = {
         val finished0 =
-          for ((name, future) <- result_futures if future.is_finished)
-          yield name ->
-            (future.join_result match {
-              case Exn.Res(result) => result
-              case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
-            })
+          for {
+            (name, _) <- result_futures
+            result <- maybe_result(name)
+          } yield name -> result
 
         val (terminated, cancelling_until1) =
           cancelling_until
@@ -826,7 +831,8 @@
 
         val finished =
           finished0 ++
-            terminated.map((name, _) => name -> Process_Result(Process_Result.RC.timeout))
+            terminated.map((name, _) =>
+              name -> maybe_result(name).getOrElse(Process_Result(Process_Result.RC.timeout)))
 
         val state1 =
           copy(
@@ -850,9 +856,7 @@
             if do_cancel(process_future)
           } yield name -> (Time.now() + cancel_timeout)
 
-        copy(
-          process_futures.filterNot((name, _) => cancelled.contains(name)),
-          cancelling_until = cancelling_until ++ cancelling_until1)
+        copy(cancelling_until = cancelling_until ++ cancelling_until1)
       }
     }
   }
@@ -1021,7 +1025,20 @@
 
     override def stopped(state: Runner.State): Boolean = progress.stopped && state.is_empty
 
-    def init: Runner.State = Runner.State.init(store.options)
+    def init: Runner.State = synchronized_database("init") {
+      for ((name, job) <- _state.running) {
+        echo("Cleaned up job " + job.uuid)
+
+        val report = store.report(job.kind, job.id)
+
+        _state = _state
+          .remove_running(job.name)
+          .add_finished(report.result(Some(job.uuid), job.user))
+      }
+
+      Runner.State.init(store.options)
+    }
+
     def loop_body(state: Runner.State): Runner.State = {
       val state1 =
         if (progress.stopped) state
@@ -1498,11 +1515,14 @@
 html { background-color: white; }"""))
     }
 
+    override def close(): Unit = {
+      server.stop()
+      super.close()
+    }
+
     def init: Unit = server.start()
-    def loop_body(u: Unit): Unit = {
-      if (progress.stopped) server.stop()
-      else synchronized_database("iterate") { cache.update() }
-    }
+    def loop_body(u: Unit): Unit =
+      if (!progress.stopped) synchronized_database("iterate") { cache.update() }
   }
 
 
diff -r 07c51801c2ea -r f38e59e1c019 src/Pure/General/latex.ML
--- a/src/Pure/General/latex.ML	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Pure/General/latex.ML	Fri Aug 30 10:44:48 2024 +0100
@@ -251,7 +251,9 @@
   else if s = Markup.keyword2N then keyword_markup
   else Markup.no_output;
 
-val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
+fun latex_escape ss = Symbol.latex :: Symbol.open_ :: ss @ [Symbol.close];
+
+val _ = Output.add_mode latexN latex_output latex_escape;
 val _ = Markup.add_mode latexN latex_markup;
 
 val _ = Pretty.add_mode latexN
diff -r 07c51801c2ea -r f38e59e1c019 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Pure/General/output.ML	Fri Aug 30 10:44:48 2024 +0100
@@ -17,11 +17,11 @@
   include BASIC_OUTPUT
   type output = string
   val default_output: string -> output * int
-  val default_escape: output -> string
-  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
+  val default_escape: output list -> string list
+  val add_mode: string -> (string -> output * int) -> (output list -> string list) -> unit
   val output_width: string -> output * int
   val output: string -> output
-  val escape: output -> string
+  val escape: output list -> string list
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
@@ -66,7 +66,7 @@
 type output = string;  (*raw system output*)
 
 fun default_output s = (s, size s);
-fun default_escape (s: output) = s;
+fun default_escape (ss: output list) = ss;
 
 local
   val default = {output = default_output, escape = default_escape};
diff -r 07c51801c2ea -r f38e59e1c019 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Pure/General/pretty.ML	Fri Aug 30 10:44:48 2024 +0100
@@ -65,11 +65,11 @@
   val regularN: string
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
-  val output: int option -> T -> Output.output
+  val output: int option -> T -> Output.output list
   val string_of_margin: int -> T -> string
   val string_of: T -> string
   val writeln: T -> unit
-  val symbolic_output: T -> Output.output
+  val symbolic_output: T -> Output.output list
   val symbolic_string_of: T -> string
   val unformatted_string_of: T -> string
   val markup_chunks: Markup.T -> T list -> T
@@ -359,15 +359,15 @@
   then symbolic prt
   else formatted (the_default (! margin_default) margin) prt;
 
-val output = Buffer.content oo output_buffer;
-fun string_of_margin margin = Output.escape o output (SOME margin);
-val string_of = Output.escape o output NONE;
-val writeln = Output.writeln o string_of;
+val output = Buffer.contents oo output_buffer;
+fun string_of_margin margin = implode o Output.escape o output (SOME margin);
+val string_of = implode o Output.escape o output NONE;
+val writeln = Output.writelns o Output.escape o output NONE;
 
-val symbolic_output = Buffer.content o symbolic;
-val symbolic_string_of = Output.escape o symbolic_output;
+val symbolic_output = Buffer.contents o symbolic;
+val symbolic_string_of = implode o Output.escape o symbolic_output;
 
-val unformatted_string_of = Output.escape o Buffer.content o unformatted;
+val unformatted_string_of = implode o Output.escape o Buffer.contents o unformatted;
 
 
 (* chunks *)
diff -r 07c51801c2ea -r f38e59e1c019 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 30 10:44:48 2024 +0100
@@ -864,8 +864,8 @@
 val enclose = output #-> Library.enclose;
 
 fun markup m =
-  let val (bg, en) = output m
-  in Library.enclose (Output.escape bg) (Output.escape en) end;
+  let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode);
+  in Library.enclose bg en end;
 
 val markups = fold_rev markup;
 
diff -r 07c51801c2ea -r f38e59e1c019 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 30 10:44:48 2024 +0100
@@ -766,7 +766,7 @@
       if show_markup andalso not show_types then
         let
           val ((bg1, bg2), en) = typing_elem;
-          val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
+          val bg = implode (bg1 :: Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) @ [bg2]);
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end
       else NONE
@@ -775,7 +775,7 @@
       if show_markup andalso not show_sorts then
         let
           val ((bg1, bg2), en) = sorting_elem;
-          val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
+          val bg = implode (bg1 :: Pretty.symbolic_output (pretty_typ_ast Markup.empty s) @ [bg2]);
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end
       else NONE
diff -r 07c51801c2ea -r f38e59e1c019 src/ZF/List.thy
--- a/src/ZF/List.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/ZF/List.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -13,15 +13,18 @@
 datatype
   "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)")
 
+notation Nil (\<open>[]\<close>)
 
+nonterminal list_args
 syntax
- "_Nil" :: i  (\<open>[]\<close>)
- "_List" :: "is \<Rightarrow> i"  (\<open>[(_)]\<close>)
-syntax_consts "_List" \<rightleftharpoons> Cons
+  "" :: "i \<Rightarrow> list_args"  (\<open>_\<close>)
+  "_List_args" :: "[i, list_args] \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
+  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(_)]\<close>)
+syntax_consts
+  "_List_args" "_List" \<rightleftharpoons> Cons
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
-  "[]"          == "CONST Nil"
 
 consts
   length :: "i\<Rightarrow>i"
diff -r 07c51801c2ea -r f38e59e1c019 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Fri Aug 30 10:16:48 2024 +0100
+++ b/src/ZF/ZF_Base.thy	Fri Aug 30 10:44:48 2024 +0100
@@ -129,13 +129,13 @@
 definition succ :: "i \<Rightarrow> i"
   where "succ(i) \<equiv> cons(i, i)"
 
-nonterminal "is"
+nonterminal "finset_args"
 syntax
-  "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
-  "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
-  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(_)}\<close>)
+  "" :: "i \<Rightarrow> finset_args"  (\<open>_\<close>)
+  "_Finset_args" :: "[i, finset_args] \<Rightarrow> finset_args"  (\<open>_,/ _\<close>)
+  "_Finset" :: "finset_args \<Rightarrow> i"  (\<open>{(_)}\<close>)
 syntax_consts
-  "_Finset" == cons
+  "_Finset_args" "_Finset" == cons
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
@@ -192,19 +192,26 @@
 definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
   where "split(c) \<equiv> \<lambda>p. c(fst(p), snd(p))"
 
+nonterminal "tuple_args"
+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>)
+syntax_consts
+  "_Tuple_args" "_Tuple" == Pair
+translations
+  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
+  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
+
 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
 nonterminal patterns
 syntax
   "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open>\<langle>_\<rangle>\<close>)
   ""          :: "pttrn \<Rightarrow> patterns"         (\<open>_\<close>)
   "_patterns" :: "[pttrn, patterns] \<Rightarrow> patterns"  (\<open>_,/_\<close>)
-  "_Tuple"    :: "[i, is] \<Rightarrow> i"              (\<open>\<langle>(_,/ _)\<rangle>\<close>)
 syntax_consts
-  "_pattern" "_patterns" == split and
-  "_Tuple" == Pair
+  "_pattern" "_patterns" == split
 translations
-  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
-  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
   "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
   "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
 
@@ -300,7 +307,7 @@
   "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3PROD _:_./ _)\<close> 10)
   "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3SUM _:_./ _)\<close> 10)
   "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3lam _:_./ _)\<close> 10)
-  "_Tuple"    :: "[i, is] \<Rightarrow> i"              (\<open><(_,/ _)>\<close>)
+  "_Tuple"    :: "[i, tuple_args] \<Rightarrow> i"      (\<open><(_,/ _)>\<close>)
   "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open><_>\<close>)