# HG changeset patch
# User haftmann
# Date 1548004475 0
# Node ID 4d95261fab5af9384dc05793482ddb86307fb95c
# Parent  9fd395ff57bcfc83430ce19c42b198911dea89e9
more conventional syntax for code_stmts antiquotation

diff -r 9fd395ff57bc -r 4d95261fab5a NEWS
--- a/NEWS	Sun Jan 20 21:26:15 2019 +0100
+++ b/NEWS	Sun Jan 20 17:14:35 2019 +0000
@@ -85,6 +85,9 @@
 proper module frame, nothing is added magically any longer.
 INCOMPATIBILITY.
 
+* Code generation: slightly more conventional syntax for
+'code_stmts' antiquotation.  Minor INCOMPATIBILITY.
+
 * Simplified syntax setup for big operators under image. In rare
 situations, type conversions are not inserted implicitly any longer
 and need to be given explicitly. Auxiliary abbreviations INFIMUM,
diff -r 9fd395ff57bc -r 4d95261fab5a src/Doc/Codegen/Foundations.thy
--- a/src/Doc/Codegen/Foundations.thy	Sun Jan 20 21:26:15 2019 +0100
+++ b/src/Doc/Codegen/Foundations.thy	Sun Jan 20 17:14:35 2019 +0000
@@ -191,7 +191,7 @@
 \<close>
 
 text %quote \<open>
-  @{code_stmts dequeue (consts) dequeue (Haskell)}
+  @{code_stmts dequeue constant: dequeue (Haskell)}
 \<close>
 
 text \<open>
@@ -283,7 +283,7 @@
 \<close>
 
 text %quote \<open>
-  @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
+  @{code_stmts strict_dequeue constant: strict_dequeue (Haskell)}
 \<close>
 
 text \<open>
@@ -325,7 +325,7 @@
 \<close>
 
 text %quote \<open>
-  @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
+  @{code_stmts strict_dequeue' constant: empty_queue strict_dequeue' (Haskell)}
 \<close>
 
 text \<open>
diff -r 9fd395ff57bc -r 4d95261fab5a src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Sun Jan 20 21:26:15 2019 +0100
+++ b/src/Doc/Codegen/Further.thy	Sun Jan 20 17:14:35 2019 +0000
@@ -194,7 +194,7 @@
 \<close>
 
 text %quote \<open>
-  @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
+  @{code_stmts funpows constant: Nat.funpow funpows (Haskell)}
 \<close>
 
 
diff -r 9fd395ff57bc -r 4d95261fab5a src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Sun Jan 20 21:26:15 2019 +0100
+++ b/src/Doc/Codegen/Refinement.thy	Sun Jan 20 17:14:35 2019 +0000
@@ -32,7 +32,7 @@
 \<close>
 
 text %quote \<open>
-  @{code_stmts fib (consts) fib (Haskell)}
+  @{code_stmts fib constant: fib (Haskell)}
 \<close>
 
 text \<open>
@@ -69,7 +69,7 @@
 \<close>
 
 text %quote \<open>
-  @{code_stmts fib (consts) fib fib_step (Haskell)}
+  @{code_stmts fib constant: fib fib_step (Haskell)}
 \<close>
 
 
diff -r 9fd395ff57bc -r 4d95261fab5a src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jan 20 21:26:15 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Jan 20 17:14:35 2019 +0000
@@ -513,25 +513,29 @@
   check_code ctxt all_public
     (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
 
+val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) =
+  (\<^keyword>\<open>constant\<close>, \<^keyword>\<open>type_constructor\<close>, \<^keyword>\<open>type_class\<close>,
+    \<^keyword>\<open>class_relation\<close>, \<^keyword>\<open>class_instance\<close>, \<^keyword>\<open>code_module\<close>);
+
 local
 
 val parse_const_terms = Scan.repeat1 Args.term
   >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
 
-fun parse_names category parse internalize mark_symbol =
-  Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
+fun parse_names keyword parse internalize mark_symbol =
+  Scan.lift (keyword --| Args.colon) |-- Scan.repeat1 parse
   >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
 
-val parse_consts = parse_names "consts" Args.term
+val parse_consts = parse_names constantK Args.term
   (Code.check_const o Proof_Context.theory_of) Constant;
 
-val parse_types = parse_names "types" (Scan.lift Args.name)
+val parse_types = parse_names type_constructorK (Scan.lift Args.name)
   (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
 
-val parse_classes = parse_names "classes" (Scan.lift Args.name)
+val parse_classes = parse_names type_classK (Scan.lift Args.name)
   (Sign.intern_class o Proof_Context.theory_of) Type_Class;
 
-val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
+val parse_instances = parse_names class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
   (fn ctxt => fn (raw_tyco, raw_class) =>
     let
       val thy = Proof_Context.theory_of ctxt;
@@ -646,10 +650,6 @@
 
 (** Isar setup **)
 
-val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) =
-  (\<^keyword>\<open>constant\<close>, \<^keyword>\<open>type_constructor\<close>, \<^keyword>\<open>type_class\<close>,
-    \<^keyword>\<open>class_relation\<close>, \<^keyword>\<open>class_instance\<close>, \<^keyword>\<open>code_module\<close>);
-
 local
 
 val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant;