reorganized signature of ML_Context;

--- a/doc-src/antiquote_setup.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/doc-src/antiquote_setup.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -36,7 +36,7 @@
       else txt1 ^ ": " ^ txt2;
     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     val _ = writeln (ml (txt1, txt2));
-    val _ = ML_Context.use_mltext false Position.none (ml (txt1, txt2)) (SOME (Context.Proof ctxt));
+    val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
   in
     "\\indexml" ^ kind ^ enclose "{" "}"
       (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^

--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -135,7 +135,7 @@
 (* generic_setup *)
 
 fun generic_setup (txt, pos) =
-  ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
+  ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup" txt
   |> Context.theory_map;
 
 
@@ -152,37 +152,42 @@
 in
 
 fun parse_ast_translation (a, (txt, pos)) =
-  txt |> ML_Context.use_let pos ("val parse_ast_translation: (string * (" ^ advancedT a ^
+  txt |> ML_Context.expression pos
+    ("val parse_ast_translation: (string * (" ^ advancedT a ^
       "Syntax.ast list -> Syntax.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   |> Context.theory_map;
 
 fun parse_translation (a, (txt, pos)) =
-  txt |> ML_Context.use_let pos ("val parse_translation: (string * (" ^ advancedT a ^
+  txt |> ML_Context.expression pos
+    ("val parse_translation: (string * (" ^ advancedT a ^
       "term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
   |> Context.theory_map;
 
 fun print_translation (a, (txt, pos)) =
-  txt |> ML_Context.use_let pos ("val print_translation: (string * (" ^ advancedT a ^
+  txt |> ML_Context.expression pos
+    ("val print_translation: (string * (" ^ advancedT a ^
       "term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
   |> Context.theory_map;
 
 fun print_ast_translation (a, (txt, pos)) =
-  txt |> ML_Context.use_let pos ("val print_ast_translation: (string * (" ^ advancedT a ^
+  txt |> ML_Context.expression pos
+    ("val print_ast_translation: (string * (" ^ advancedT a ^
       "Syntax.ast list -> Syntax.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   |> Context.theory_map;
 
 fun typed_print_translation (a, (txt, pos)) =
-  txt |> ML_Context.use_let pos ("val typed_print_translation: (string * (" ^ advancedT a ^
+  txt |> ML_Context.expression pos
+    ("val typed_print_translation: (string * (" ^ advancedT a ^
       "bool -> typ -> term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
   |> Context.theory_map;
 
 fun token_translation (txt, pos) =
-  txt |> ML_Context.use_let pos
+  txt |> ML_Context.expression pos
     "val token_translation: (string * string * (string -> output * int)) list"
       "Context.map_theory (Sign.add_tokentrfuns token_translation)"
   |> Context.theory_map;
@@ -205,8 +210,7 @@
     \in\n\
     \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
     \end;\n";
-  in ML_Context.use_mltext_update false pos txt end
-  |> Context.theory_map;
+  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
 
 
 (* axioms *)
@@ -233,7 +237,8 @@
 (* declarations *)
 
 fun declaration (txt, pos) =
-  txt |> ML_Context.use_let pos "val declaration: Morphism.declaration"
+  txt |> ML_Context.expression pos
+    "val declaration: Morphism.declaration"
     "Context.map_proof (LocalTheory.declaration declaration)"
   |> Context.proof_map;
 
@@ -241,7 +246,7 @@
 (* simprocs *)
 
 fun simproc_setup name lhss (proc, pos) identifier =
-  ML_Context.use_let pos
+  ML_Context.expression pos
     "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
   ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
     \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
@@ -382,12 +387,12 @@
   Context.setmp_thread_data (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
 
 (*passes changes of theory context*)
-fun use_mltext_theory (txt, pos) =
-  Toplevel.theory' (fn int => Context.theory_map (ML_Context.use_mltext_update int pos txt));
+fun use_mltext_theory (txt, pos) = Toplevel.theory' (fn int =>
+  Context.theory_map (ML_Context.exec (fn () => ML_Context.eval int pos txt)));
 
 (*ignore result theory context*)
 fun use_mltext verbose (txt, pos) = Toplevel.keep' (fn int => fn state =>
-  (ML_Context.use_mltext (verbose andalso int) pos txt (try Toplevel.generic_theory_of state)));
+  (ML_Context.eval_in (try Toplevel.generic_theory_of state) (verbose andalso int) pos txt));
 
 val use_commit = Toplevel.imperative Secure.commit;
 

--- a/src/Pure/Isar/method.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/Isar/method.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -354,9 +354,9 @@
 fun set_tactic f = tactic_ref := f;
 
 fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () =>
-  (ML_Context.use_mltext false pos
+  (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos
     ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
-      ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
+      ^ txt ^ "\nin Method.set_tactic tactic end");
     Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
 
 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
@@ -447,7 +447,7 @@
 (* method_setup *)
 
 fun method_setup name (txt, pos) cmt =
-  ML_Context.use_let pos
+  ML_Context.expression pos
     "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
     "Context.map_theory (Method.add_method method)"
     ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")

--- a/src/Pure/ML/ml_context.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -21,7 +21,7 @@
   val the_generic_context: unit -> Context.generic
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
-  val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
+  val exec: (unit -> unit) -> Context.generic -> Context.generic
   val stored_thms: thm list ref
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
@@ -34,12 +34,12 @@
       (string * string * string) * (Context.generic * Args.T list)) -> unit
   val eval_antiquotes_fn: (string * Position.T -> string * string) ref  (* FIXME tmp *)
   val trace: bool ref
-  val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit
-  val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic
-  val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic
-  val use: Path.T -> unit
+  val eval: bool -> Position.T -> string -> unit
+  val eval_file: Path.T -> unit
+  val eval_in: Context.generic option -> bool -> Position.T -> string -> unit
   val evaluate: (string -> unit) * (string -> 'b) -> bool ->
     string * (unit -> 'a) option ref -> string -> 'a
+  val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
 end
 
 structure ML_Context: ML_CONTEXT =
@@ -51,10 +51,10 @@
 val the_global_context = Context.theory_of o the_generic_context;
 val the_local_context = Context.proof_of o the_generic_context;
 
-fun pass_context context f x =
-  (case Context.setmp_thread_data (SOME context) (fn () => (f x, Context.thread_data ())) () of
-    (y, SOME context') => (y, context')
-  | (_, NONE) => error "Lost context after evaluation");
+fun exec (e: unit -> unit) context =
+  (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
+    SOME context' => context'
+  | NONE => error "Missing context after execution");
 
 
 (* theorem bindings *)
@@ -200,18 +200,11 @@
 
 (* ML evaluation *)
 
-fun use_mltext verbose pos txt opt_context =
-  Context.setmp_thread_data opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) ();
-
-fun use_mltext_update verbose pos txt context =
-  #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ());
+val eval = eval_wrapper Output.ml_output;
+fun eval_file path = eval true (Position.path path) (File.read path);
 
-fun use_let pos bind body txt =
-  use_mltext_update false pos
-    ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
-      " end (ML_Context.the_generic_context ())));");
-
-fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path);
+fun eval_in context verbose pos txt =
+  Context.setmp_thread_data context (fn () => eval verbose pos txt) ();
 
 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   let
@@ -220,6 +213,11 @@
       ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
   in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
 
+fun expression pos bind body txt =
+  exec (fn () => eval false pos
+    ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+      " end (ML_Context.the_generic_context ())));"));
+
 
 (* basic antiquotations *)
 

--- a/src/Pure/Thy/thy_info.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -546,9 +546,8 @@
       |> Present.begin_theory update_time dir uses;
 
     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
-    val ((), theory'') =
-      ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
-      ||> Context.the_theory;
+    val theory'' =
+      Context.theory_map (ML_Context.exec (fn () => List.app (load_file false) uses_now)) theory';
   in theory'' end;
 
 fun end_theory theory =

--- a/src/Pure/Thy/thy_load.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -119,7 +119,7 @@
 fun load_ml dir raw_path =
   (case check_ml dir raw_path of
     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
-  | SOME (path, id) => (ML_Context.use path; (path, id)));
+  | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
 
 (*dependent on outer syntax*)
 val load_thy_fn =

--- a/src/Pure/Thy/thy_output.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -502,7 +502,7 @@
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
 fun output_ml ml src ctxt (txt, pos) =
- (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt));
+ (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
   (if ! source then str_of_source src else txt)
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"

--- a/src/Pure/codegen.ML	Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/codegen.ML	Fri Mar 28 00:02:54 2008 +0100
@@ -963,7 +963,7 @@
                   [Pretty.str "]"])]]),
           Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
+    val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (if quiet then ()
@@ -1053,7 +1053,7 @@
               [Pretty.str "(result ())"],
             Pretty.str ");"]) ^
         "\n\nend;\n";
-      val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
+      val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
     in !eval_result end) ();
   in e () end;
 
@@ -1148,8 +1148,9 @@
        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
-         NONE => ML_Context.use_mltext false Position.none (space_implode "\n" (map snd code))
-           (SOME (Context.Theory thy))
+         NONE =>
+           ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
+             (space_implode "\n" (map snd code))
        | SOME fname =>
            if lib then
              app (fn (name, s) => File.write