--- 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>
--- 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
--- 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"
--- 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>]"
--- 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"
--- 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"
--- 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
--- 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"
--- 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"
--- 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"
--- 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 {||}"
--- 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
--- 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 {#}"
--- 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)"
--- 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#[]"
--- 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
--- 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
--- 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 {||}"
--- 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 {||}"
--- 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"
--- 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 {}"
--- 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>"
--- 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() }
}
--- 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
--- 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};
--- 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 *)
--- 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;
--- 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
--- 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"
--- 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>)