# HG changeset patch
# User haftmann
# Date 1735803475 -3600
# Node ID 7beb0cf382921ce729c1cd610e7aca16d3294555
# Parent  53fea2ccab1965faa50b2884cc1c1894b45c869c
refined syntax for code_reserved

diff -r 53fea2ccab19 -r 7beb0cf38292 NEWS
--- a/NEWS	Thu Jan 02 08:37:52 2025 +0100
+++ b/NEWS	Thu Jan 02 08:37:55 2025 +0100
@@ -222,6 +222,9 @@
 
 *** HOL ***
 
+* Code generator: `code_reserved` now uses brackets for target languages,
+similar to `code_printing.
+
 * Sledgehammer:
   - Added instantiations of facts using the "of" attribute
     (e.g. "assms(1)[of x]"), which can be activated using the
diff -r 53fea2ccab19 -r 7beb0cf38292 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -295,7 +295,7 @@
   @{command_def "code_reserved"} command:
 \<close>
 
-code_reserved %quote "\<SMLdummy>" bool true false andalso
+code_reserved %quotett ("\<SMLdummy>") bool true false andalso
 
 text \<open>
   \noindent Next, we try to map HOL pairs to SML pairs, using the
@@ -388,7 +388,7 @@
 
   errno i = error ("Error number: " ++ show i)\<close>
 
-code_reserved %quotett Haskell Errno
+code_reserved %quotett (Haskell) Errno
 
 text \<open>
   \noindent Such named modules are then prepended to every
diff -r 53fea2ccab19 -r 7beb0cf38292 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -2314,7 +2314,7 @@
     ;
     @@{command (HOL) code_deps} (const_expr+)
     ;
-    @@{command (HOL) code_reserved} target (@{syntax string}+)
+    @@{command (HOL) code_reserved} ('(' target ')' (@{syntax string}+) + @'and')
     ;
     symbol_const: @'constant' const
     ;
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -88,7 +88,8 @@
 
 ML_file \<open>Tools/code_evaluation.ML\<close>
 
-code_reserved Eval Code_Evaluation
+code_reserved
+  (Eval) Code_Evaluation
 
 ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
 
@@ -128,7 +129,8 @@
        (term_of (- i)))"
   by (rule term_of_anything [THEN meta_eq_to_obj_eq])
 
-code_reserved Eval HOLogic
+code_reserved
+  (Eval) HOLogic
 
 
 subsection \<open>Generic reification\<close>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -780,7 +780,8 @@
 
 subsection \<open>Serializer setup for target language integers\<close>
 
-code_reserved Eval int Integer abs
+code_reserved
+  (Eval) int Integer abs
 
 code_printing
   type_constructor integer \<rightharpoonup>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -42,7 +42,7 @@
 
 text \<open>Avoid popular infix.\<close>
 
-code_reserved SML upto
+code_reserved (SML) upto
 
 text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close>
 
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/HOL.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -2074,14 +2074,10 @@
 | constant False \<rightharpoonup>
     (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
 
-code_reserved SML
-  bool true false
-
-code_reserved OCaml
-  bool
-
-code_reserved Scala
-  Boolean
+code_reserved
+  (SML) bool true false
+  and (OCaml) bool
+  and (Scala) Boolean
 
 code_printing
   constant Not \<rightharpoonup>
@@ -2101,11 +2097,9 @@
     and (Haskell) "!(if (_)/ then (_)/ else (_))"
     and (Scala) "!((_) match {/ case true => (_)/ case false => (_)/ })"
 
-code_reserved SML
-  not
-
-code_reserved OCaml
-  not
+code_reserved
+  (SML) not
+  and (OCaml) not
 
 code_identifier
   code_module Pure \<rightharpoonup>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -451,7 +451,7 @@
 code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ IntInf.toInt _,/ (_)))"
 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
 
-code_reserved SML Array
+code_reserved (SML) Array
 
 
 text \<open>OCaml\<close>
@@ -467,7 +467,7 @@
 code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Z.to'_int/ _)/ _)"
 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
 
-code_reserved OCaml Array
+code_reserved (OCaml) Array
 
 
 text \<open>Haskell\<close>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -565,7 +565,7 @@
 writeArray :: STArray s a -> Integer -> a -> ST s ()
 writeArray = Data.Array.ST.writeArray\<close>
 
-code_reserved Haskell Heap
+code_reserved (Haskell) Heap
 
 text \<open>Monad\<close>
 
@@ -620,7 +620,7 @@
 
 \<close>
 
-code_reserved Scala Heap Ref Array
+code_reserved (Scala) Heap Ref Array
 
 code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
 code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -284,7 +284,7 @@
 code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
 
-code_reserved Eval Unsynchronized
+code_reserved (Eval) Unsynchronized
 
 
 text \<open>OCaml\<close>
@@ -296,7 +296,7 @@
 code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
 
-code_reserved OCaml ref
+code_reserved (OCaml) ref
 
 
 text \<open>Haskell\<close>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -655,7 +655,7 @@
     return a
   }"
 
-code_reserved SML upto
+code_reserved (SML) upto
 
 definition "example = do {
     a \<leftarrow> Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -956,7 +956,7 @@
     return zs
   })"
 
-code_reserved SML upto
+code_reserved (SML) upto
 
 ML_val \<open>@{code test_1} ()\<close>
 ML_val \<open>@{code test_2} ()\<close>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Code_Lazy.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -116,7 +116,7 @@
 | constant force \<rightharpoonup> (SML) "Lazy.force"
 | constant termify_lazy \<rightharpoonup> (SML) "Lazy.termify'_lazy"
 
-code_reserved SML Lazy
+code_reserved (SML) Lazy
 
 code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe
   implementation of lazy from \<^file>\<open>~~/src/Pure/Concurrent/lazy.ML\<close>\<close>
@@ -137,7 +137,7 @@
 end;\<close> for constant termify_lazy
 | constant termify_lazy \<rightharpoonup> (Eval) "Termify'_Lazy.termify'_lazy"
 
-code_reserved Eval Termify_Lazy
+code_reserved (Eval) Termify_Lazy
 
 code_printing
   type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
@@ -161,7 +161,7 @@
 end;;\<close> for constant termify_lazy
 | constant termify_lazy \<rightharpoonup> (OCaml) "Termify'_Lazy.termify'_lazy"
 
-code_reserved OCaml Lazy Termify_Lazy
+code_reserved (OCaml) Lazy Termify_Lazy
 
 
 code_printing
@@ -175,7 +175,7 @@
 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
 
-code_reserved Haskell Lazy
+code_reserved (Haskell) Lazy
 
 code_printing
   code_module Lazy \<rightharpoonup> (Scala) 
@@ -220,7 +220,7 @@
 | constant force \<rightharpoonup> (Scala) "Lazy.force"
 | constant termify_lazy \<rightharpoonup> (Scala) "Lazy.termify'_lazy"
 
-code_reserved Scala Lazy
+code_reserved (Scala) Lazy
 
 text \<open>Make evaluation with the simplifier respect \<^term>\<open>delay\<close>s.\<close>
 
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -82,7 +82,7 @@
   arccos
   arctan]]
 
-code_reserved SML Real
+code_reserved (SML) Real
 
 code_printing
   type_constructor real \<rightharpoonup>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Debug.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -39,7 +39,6 @@
 | constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
 | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
 
-code_reserved Eval Output Timing
+code_reserved (Eval) Output Timing
 
 end
-
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/IArray.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -177,7 +177,7 @@
 lists first. Arrays could be converted back into lists for printing if they
 were wrapped up in an additional constructor.\<close>
 
-code_reserved SML Vector
+code_reserved (SML) Vector
 
 code_printing
   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
@@ -222,7 +222,7 @@
 
 }\<close> for type_constructor iarray constant IArray IArray.tabulate IArray.sub' IArray.length'
 
-code_reserved Haskell IArray_Impl
+code_reserved (Haskell) IArray_Impl
 
 code_printing
   type_constructor iarray \<rightharpoonup> (Haskell) "IArray.IArray _"
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Parallel.thy
--- a/src/HOL/Library/Parallel.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Parallel.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -23,7 +23,7 @@
 | constant fork \<rightharpoonup> (Eval) "Future.fork"
 | constant join \<rightharpoonup> (Eval) "Future.join"
 
-code_reserved Eval Future future
+code_reserved (Eval) Future future
 
 
 subsection \<open>Parallel lists\<close>
@@ -50,7 +50,7 @@
 | constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
 | constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
 
-code_reserved Eval Par_List
+code_reserved (Eval) Par_List
 
 
 hide_const (open) fork join map exists forall
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Limited_Sequence.thy
--- a/src/HOL/Limited_Sequence.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Limited_Sequence.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -200,8 +200,8 @@
 end;
 \<close>
 
-code_reserved Eval Limited_Sequence
-
+code_reserved
+  (Eval) Limited_Sequence
 
 hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map
   pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
@@ -213,4 +213,3 @@
   neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
 
 end
-
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/List.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -8089,11 +8089,9 @@
 
 setup \<open>fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]\<close>
 
-code_reserved SML
-  list
-
-code_reserved OCaml
-  list
+code_reserved
+  (SML) list
+  and (OCaml) list
 
 
 subsubsection \<open>Use convenient predefined operations\<close>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Option.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -373,13 +373,9 @@
 | constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
     (Haskell) infix 4 "=="
 
-code_reserved SML
-  option NONE SOME
-
-code_reserved OCaml
-  option None Some
-
-code_reserved Scala
-  Option None Some
+code_reserved
+  (SML) option NONE SOME
+  and (OCaml) option None Some
+  and (Scala) Option None Some
 
 end
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Product_Type.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -195,14 +195,10 @@
 | constant "HOL.equal :: unit \<Rightarrow> unit \<Rightarrow> bool" \<rightharpoonup>
     (Haskell) infix 4 "=="
 
-code_reserved SML
-  unit
-
-code_reserved OCaml
-  unit
-
-code_reserved Scala
-  Unit
+code_reserved
+  (SML) unit
+  and (OCaml) unit
+  and (Scala) Unit
 
 
 subsection \<open>The product type\<close>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -22,7 +22,8 @@
 | type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
 | constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
 
-code_reserved Haskell_Quickcheck Typerep
+code_reserved
+  (Haskell_Quickcheck) Typerep
 
 code_printing
   type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -17,7 +17,8 @@
 code_printing
   constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
 
-code_reserved Quickcheck Match
+code_reserved
+  (Quickcheck) Match
 
 subsection \<open>The \<open>random\<close> class\<close>
 
@@ -271,7 +272,8 @@
   for this reason we use a distinguished target \<open>Quickcheck\<close>
   not spoiling the regular trusted code generation\<close>
 
-code_reserved Quickcheck Random_Generators
+code_reserved
+  (Quickcheck) Random_Generators
 
 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
 
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/String.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -721,10 +721,11 @@
 
 end
 
-code_reserved SML string String Char Str_Literal
-code_reserved OCaml string String Char Str_Literal
-code_reserved Haskell Prelude
-code_reserved Scala string
+code_reserved
+  (SML) string String Char Str_Literal
+  and (OCaml) string String Char Str_Literal
+  and (Haskell) Prelude
+  and (Scala) string
 
 code_identifier
   code_module String \<rightharpoonup>
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Typerep.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -90,7 +90,8 @@
   type_constructor typerep \<rightharpoonup> (Eval) "Term.typ"
 | constant Typerep \<rightharpoonup> (Eval) "Term.Type/ (_, _)"
 
-code_reserved Eval Term
+code_reserved
+  (Eval) Term
 
 hide_const (open) typerep Typerep
 
diff -r 53fea2ccab19 -r 7beb0cf38292 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Jan 02 08:37:55 2025 +0100
@@ -739,10 +739,9 @@
 in
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close>
-    "declare words as reserved for target language"
-    (Parse.name -- Scan.repeat1 Parse.name
-      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
+  Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close> "declare words as reserved for target language"
+    (Parse.and_list1 (\<^keyword>\<open>(\<close> |-- (Parse.name --| \<^keyword>\<open>)\<close> -- Scan.repeat1 Parse.name))
+      >> (Toplevel.theory o fold (fn (target, reserveds) => fold (add_reserved target) reserveds)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_identifier\<close> "declare mandatory names for code symbols"