# 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)))));