# HG changeset patch
# User wenzelm
# Date 1344716266 -7200
# Node ID 37cd53e69840dfea3a28b0e478af0c025155e593
# Parent  92ceb058391f4043360a329f717f89f0c22f422e
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

diff -r 92ceb058391f -r 37cd53e69840 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/FOL/FOL.thy	Sat Aug 11 22:17:46 2012 +0200
@@ -184,7 +184,7 @@
 
 setup {*
   ML_Antiquote.value @{binding claset}
-    (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())")
+    (Scan.succeed "Cla.claset_of ML_context")
 *}
 
 setup Cla.setup
diff -r 92ceb058391f -r 37cd53e69840 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/HOL/HOL.thy	Sat Aug 11 22:17:46 2012 +0200
@@ -847,7 +847,7 @@
 
 setup {*
   ML_Antiquote.value @{binding claset}
-    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())")
+    (Scan.succeed "Classical.claset_of ML_context")
 *}
 
 setup Classical.setup
diff -r 92ceb058391f -r 37cd53e69840 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Aug 11 22:17:46 2012 +0200
@@ -38,8 +38,8 @@
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
-  val diag_state: unit -> Toplevel.state
-  val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
+  val diag_state: Proof.context -> Toplevel.state
+  val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
@@ -297,18 +297,18 @@
     |> Option.map (Context.proof_of #> Diag_State.put state)
   in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
 
-fun diag_state () = Diag_State.get (ML_Context.the_local_context ());
+val diag_state = Diag_State.get;
 
-fun diag_goal () =
-  Proof.goal (Toplevel.proof_of (diag_state ()))
+fun diag_goal ctxt =
+  Proof.goal (Toplevel.proof_of (diag_state ctxt))
     handle Toplevel.UNDEF => error "No goal present";
 
 val _ =
   Context.>> (Context.map_theory
    (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
-      (Scan.succeed "Isar_Cmd.diag_state ()") #>
+      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
     ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
-      (Scan.succeed "Isar_Cmd.diag_goal ()")));
+      (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
 
 
 (* present draft files *)
diff -r 92ceb058391f -r 37cd53e69840 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Aug 11 22:17:46 2012 +0200
@@ -20,10 +20,12 @@
 
 (* ML names *)
 
+val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
+
 structure Names = Proof_Data
 (
   type T = Name.context;
-  fun init _ = ML_Syntax.reserved;
+  fun init _ = init_context;
 );
 
 fun variant a ctxt =
@@ -73,7 +75,7 @@
       "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
     || Scan.succeed "ML_Context.the_global_context ()") #>
 
-  value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
+  value (Binding.name "context") (Scan.succeed "ML_context") #>
 
   inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
diff -r 92ceb058391f -r 37cd53e69840 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/Pure/ML/ml_context.ML	Sat Aug 11 22:17:46 2012 +0200
@@ -130,7 +130,11 @@
   Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
 
-val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
+val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
+val begin_env =
+  ML_Lex.tokenize
+    "structure Isabelle =\nstruct\nval ML_context = ML_Context.the_local_context ()\n";
+
 val end_env = ML_Lex.tokenize "end;";
 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
 
@@ -141,7 +145,7 @@
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
     val ((ml_env, ml_body), opt_ctxt') =
       if forall Antiquote.is_text ants
-      then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
+      then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
           val ctxt =
@@ -167,9 +171,9 @@
                 (no_decl, (Stack.pop scope, background));
 
           val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
-          val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
-        in (ml, SOME (Context.Proof ctxt')) end;
-  in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
+          val (ml_env, ml_body) = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
+        in ((begin_env @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
+  in ((ml_env @ end_env, ml_body), opt_ctxt') end;
 
 val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
 val trace = Config.bool trace_raw;
diff -r 92ceb058391f -r 37cd53e69840 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/Pure/ML/ml_thms.ML	Sat Aug 11 22:17:46 2012 +0200
@@ -46,7 +46,7 @@
           val (a, background') = background
             |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
           val ml =
-            ("val " ^ a ^ " = ML_Thms.the_attributes (ML_Context.the_local_context ()) " ^
+            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
               string_of_int i ^ ";\n", "Isabelle." ^ a);
         in (K ml, background') end))));
 
@@ -54,8 +54,7 @@
 (* fact references *)
 
 fun thm_bind kind a i =
-  "val " ^ a ^ " = ML_Thms.the_" ^ kind ^
-    " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
+  "val " ^ a ^ " = ML_Thms.the_" ^ kind ^ " ML_context " ^ string_of_int i ^ ";\n";
 
 fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
   (fn _ => scan >> (fn ths => fn background =>
diff -r 92ceb058391f -r 37cd53e69840 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Aug 11 21:32:46 2012 +0200
+++ b/src/Pure/simplifier.ML	Sat Aug 11 22:17:46 2012 +0200
@@ -154,7 +154,7 @@
 
 val _ = Context.>> (Context.map_theory
   (ML_Antiquote.value (Binding.name "simpset")
-    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())")));
+    (Scan.succeed "Simplifier.simpset_of ML_context")));
 
 
 (* global simpset *)
@@ -180,7 +180,7 @@
    (ML_Antiquote.value (Binding.name "simproc")
       (Args.context -- Scan.lift (Parse.position Args.name)
         >> (fn (ctxt, name) =>
-          "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
+          "Simplifier.the_simproc ML_context " ^
             ML_Syntax.print_string (check_simproc ctxt name)))));