# HG changeset patch
# User wenzelm
# Date 1394657928 -3600
# Node ID 451d5b73f8cf1a58d64d8b20956b10a21aa73360
# Parent  f74d0a4d8ae389c8ae37641404c3ab7b97716521
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
added command 'print_ML_antiquotations';

diff -r f74d0a4d8ae3 -r 451d5b73f8cf NEWS
--- a/NEWS	Wed Mar 12 21:29:46 2014 +0100
+++ b/NEWS	Wed Mar 12 21:58:48 2014 +0100
@@ -437,6 +437,10 @@
 theory merge).  Note that the softer Thm.eq_thm_prop is often more
 appropriate than Thm.eq_thm.
 
+* Simplified programming interface to define ML antiquotations, see
+ML_Context.antiquotation, to make it more close to the analogous
+Thy_Output.antiquotation.  Minor INCOMPATIBILTY.
+
 
 *** System ***
 
diff -r f74d0a4d8ae3 -r 451d5b73f8cf etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Mar 12 21:29:46 2014 +0100
+++ b/etc/isar-keywords-ZF.el	Wed Mar 12 21:58:48 2014 +0100
@@ -116,6 +116,7 @@
     "pretty_setmargin"
     "prf"
     "primrec"
+    "print_ML_antiquotations"
     "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
@@ -285,6 +286,7 @@
     "locale_deps"
     "pr"
     "prf"
+    "print_ML_antiquotations"
     "print_abbrevs"
     "print_antiquotations"
     "print_attributes"
diff -r f74d0a4d8ae3 -r 451d5b73f8cf etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Mar 12 21:29:46 2014 +0100
+++ b/etc/isar-keywords.el	Wed Mar 12 21:58:48 2014 +0100
@@ -170,6 +170,7 @@
     "primcorec"
     "primcorecursive"
     "primrec"
+    "print_ML_antiquotations"
     "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
@@ -400,6 +401,7 @@
     "nitpick"
     "pr"
     "prf"
+    "print_ML_antiquotations"
     "print_abbrevs"
     "print_antiquotations"
     "print_attributes"
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 12 21:58:48 2014 +0100
@@ -842,11 +842,18 @@
       Toplevel.keep (Method.print_methods o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
+  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
+    "print document antiquotations"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
 
 val _ =
+  Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
+    "print ML antiquotations"
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
+
+val _ =
   Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
     (Scan.succeed Isar_Cmd.thy_deps);
 
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 21:58:48 2014 +0100
@@ -37,18 +37,15 @@
 (* specific antiquotations *)
 
 fun inline name scan =
-  ML_Context.add_antiq name
-    (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s)))));
+  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
 
 fun value name scan =
-  ML_Context.add_antiq name
-    (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
-      let
-        val ctxt = Context.the_proof context;
-        val (a, ctxt') = variant (Binding.name_of name) ctxt;
-        val env = "val " ^ a ^ " = " ^ s ^ ";\n";
-        val body = "Isabelle." ^ a;
-      in (Context.Proof ctxt', (K (env, body))) end)));
+  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
+    let
+      val (a, ctxt') = variant (Binding.name_of name) ctxt;
+      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
+      val body = "Isabelle." ^ a;
+    in (K (env, body), ctxt') end);
 
 
 
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Mar 12 21:58:48 2014 +0100
@@ -23,9 +23,10 @@
   val get_stored_thm: unit -> thm
   val ml_store_thms: string * thm list -> unit
   val ml_store_thm: string * thm -> unit
-  type antiq = Proof.context -> string * string
-  val add_antiq: binding -> antiq context_parser -> theory -> theory
-  val check_antiq: Proof.context -> xstring * Position.T -> string
+  val print_antiquotations: Proof.context -> unit
+  type decl = Proof.context -> string * string
+  val antiquotation: binding -> 'a context_parser ->
+    (Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory
   val trace_raw: Config.raw
   val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -95,28 +96,36 @@
 
 (** ML antiquotations **)
 
-(* antiquotation commands *)
-
-type antiq = Proof.context -> string * string;
+(* theory data *)
 
-structure Antiq_Parsers = Theory_Data
+type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
+structure Antiquotations = Theory_Data
 (
-  type T = antiq context_parser Name_Space.table;
+  type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table;
   val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of;
+val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
+
+fun add_antiquotation name f thy = thy
+  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
 
-fun add_antiq name scan thy = thy
-  |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
+fun print_antiquotations ctxt =
+  Pretty.big_list "ML antiquotations:"
+    (map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt)))
+  |> Pretty.writeln;
 
-fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
+fun apply_antiquotation src ctxt =
+  let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
+  in f src' ctxt end;
 
-fun antiquotation src ctxt =
-  let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src
-  in Args.syntax scan src' ctxt end;
+fun antiquotation name scan body =
+  add_antiquotation name
+    (fn src => fn orig_ctxt =>
+      let val (x, _) = Args.syntax scan src orig_ctxt
+      in body src x orig_ctxt end);
 
 
 (* parsing and evaluation *)
@@ -159,7 +168,8 @@
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
             | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
                 let
-                  val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+                  val (decl, ctxt') =
+                    apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
                   val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', ctxt') end;
 
@@ -210,10 +220,12 @@
   eval verbose (#pos source) (ML_Lex.read_source source);
 
 fun eval_in ctxt verbose pos ants =
-  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
+  Context.setmp_thread_data (Option.map Context.Proof ctxt)
+    (fn () => eval verbose pos ants) ();
 
 fun eval_source_in ctxt verbose source =
-  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source verbose source) ();
+  Context.setmp_thread_data (Option.map Context.Proof ctxt)
+    (fn () => eval_source verbose source) ();
 
 fun expression pos bind body ants =
   exec (fn () => eval false pos
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Mar 12 21:58:48 2014 +0100
@@ -35,11 +35,9 @@
 (* attribute source *)
 
 val _ = Theory.setup
-  (ML_Context.add_antiq @{binding attributes}
-    (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
+  (ML_Context.antiquotation @{binding attributes} (Scan.lift Parse_Spec.attribs)
+    (fn _ => fn raw_srcs => fn ctxt =>
       let
-        val ctxt = Context.the_proof context;
-
         val i = serial ();
         val srcs = map (Attrib.check_src ctxt) raw_srcs;
         val _ = map (Attrib.attribute ctxt) srcs;
@@ -48,15 +46,13 @@
         val ml =
           ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
             string_of_int i ^ ";\n", "Isabelle." ^ a);
-      in (Context.Proof ctxt', K ml) end))));
+      in (K ml, ctxt') end));
 
 
 (* fact references *)
 
-fun thm_binding kind is_single context thms =
+fun thm_binding kind is_single thms ctxt =
   let
-    val ctxt = Context.the_proof context;
-
     val initial = null (get_thmss ctxt);
     val (name, ctxt') = ML_Antiquote.variant kind ctxt;
     val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
@@ -69,15 +65,11 @@
           val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
         in (ml_env, ml_body) end
       else ("", ml_body);
-  in (Context.Proof ctxt'', decl) end;
+  in (decl, ctxt'') end;
 
 val _ = Theory.setup
-  (ML_Context.add_antiq @{binding thm}
-    (Scan.depend (fn context =>
-      Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
-   ML_Context.add_antiq @{binding thms}
-    (Scan.depend (fn context =>
-      Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
+  (ML_Context.antiquotation @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
+   ML_Context.antiquotation @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
 
 
 (* ad-hoc goals *)
@@ -87,29 +79,26 @@
 val goal = Scan.unless (by || and_) Args.name_inner_syntax;
 
 val _ = Theory.setup
-  (ML_Context.add_antiq @{binding lemma}
-    (Scan.depend (fn context =>
-      Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
-      (by |-- Method.parse -- Scan.option Method.parse)
-     >> (fn ((is_open, raw_propss), (m1, m2)) =>
-          let
-            val ctxt = Context.proof_of context;
-
-            val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
+  (ML_Context.antiquotation @{binding lemma}
+    (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
+      (by |-- Method.parse -- Scan.option Method.parse)))
+    (fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
+      let
+        val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
 
-            val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
-            val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
-            fun after_qed res goal_ctxt =
-              Proof_Context.put_thms false (Auto_Bind.thisN,
-                SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
+        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
+        fun after_qed res goal_ctxt =
+          Proof_Context.put_thms false (Auto_Bind.thisN,
+            SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
 
-            val ctxt' = ctxt
-              |> Proof.theorem NONE after_qed propss
-              |> Proof.global_terminal_proof (m1, m2);
-            val thms =
-              Proof_Context.get_fact ctxt'
-                (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
-          in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
+        val ctxt' = ctxt
+          |> Proof.theorem NONE after_qed propss
+          |> Proof.global_terminal_proof (m1, m2);
+        val thms =
+          Proof_Context.get_fact ctxt'
+            (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
+      in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
 
 end;
 
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/Pure.thy	Wed Mar 12 21:58:48 2014 +0100
@@ -78,14 +78,15 @@
   and "finally" "ultimately" :: prf_chain % "proof"
   and "back" :: prf_script % "proof"
   and "Isabelle.command" :: control
-  and "help" "print_commands" "print_options"
-    "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
+  and "help" "print_commands" "print_options" "print_context"
+    "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
-    "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
-    "print_binds" "print_facts" "print_cases" "print_statement" "thm"
-    "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
+    "print_antiquotations" "print_ML_antiquotations" "thy_deps"
+    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts"
+    "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
+    "term" "typ" "print_codesetup" "unused_thms"
     :: diag
   and "cd" :: control
   and "pwd" :: diag
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 12 21:58:48 2014 +0100
@@ -112,11 +112,11 @@
     |> Pretty.chunks |> Pretty.writeln
   end;
 
-fun antiquotation name scan out =
+fun antiquotation name scan body =
   add_command name
     (fn src => fn state => fn ctxt =>
       let val (x, ctxt') = Args.syntax scan src ctxt
-      in out {source = src, state = state, context = ctxt'} x end);
+      in body {source = src, state = state, context = ctxt'} x end);
 
 
 
diff -r f74d0a4d8ae3 -r 451d5b73f8cf src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Mar 12 21:58:48 2014 +0100
@@ -257,15 +257,12 @@
 
 in
 
-fun ml_code_antiq context raw_const =
+fun ml_code_antiq raw_const ctxt =
   let
-    val ctxt = Context.the_proof context;
     val thy = Proof_Context.theory_of ctxt;
-
     val const = Code.check_const thy raw_const;
     val is_first = is_first_occ ctxt;
-    val ctxt' = register_const const ctxt;
-  in (Context.Proof ctxt', print_code is_first const) end;
+  in (print_code is_first const, register_const const ctxt) end;
 
 end; (*local*)
 
@@ -356,9 +353,8 @@
 
 (** Isar setup **)
 
-val _ = Theory.setup
-  (ML_Context.add_antiq @{binding code}
-    (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
+val _ =
+  Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq));
 
 local