# HG changeset patch
# User wenzelm
# Date 1237840811 -3600
# Node ID beaadd5af5004f8cf3a09ec1b298e83b67c2b46c
# Parent  2f64540707d6420fa8cf0580e6b1108d30103a3d
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;

diff -r 2f64540707d6 -r beaadd5af500 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/General/secure.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -9,11 +9,8 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
-  val use_text: ML_NameSpace.nameSpace -> int * string ->
-    (string -> unit) * (string -> 'a) -> bool -> string -> unit
-  val use_file: ML_NameSpace.nameSpace ->
-    (string -> unit) * (string -> 'a) -> bool -> string -> unit
-  val use: string -> unit
+  val use_text: use_context -> int * string -> bool -> string -> unit
+  val use_file: use_context -> bool -> string -> unit
   val toplevel_pp: string list -> string -> unit
   val commit: unit -> unit
   val system_out: string -> string * int
@@ -40,23 +37,17 @@
 
 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
 
-fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
-fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
-fun raw_toplevel_pp x =
-  toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
+val raw_use_text = use_text;
+val raw_use_file = use_file;
+val raw_toplevel_pp = toplevel_pp;
 
-fun use_text ns pos pr verbose txt =
-  (secure_mltext (); raw_use_text ns pos pr verbose txt);
+fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
+fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
 
-fun use_file ns pr verbose name =
-  (secure_mltext (); raw_use_file ns pr verbose name);
-
-fun use name = use_file ML_NameSpace.global Output.ml_output true name;
-
-fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
 
 (*commit is dynamically bound!*)
-fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
+fun commit () = raw_use_text ML_Parse.global_context (0, "") false "commit();";
 
 
 (* shell commands *)
@@ -77,7 +68,8 @@
 (*override previous toplevel bindings!*)
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
-fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+fun use s = Secure.use_file ML_Parse.global_context true s
+  handle ERROR msg => (writeln msg; raise Fail "ML error");
 val toplevel_pp = Secure.toplevel_pp;
 val system_out = Secure.system_out;
 val system = Secure.system;
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/IsaMakefile	Mon Mar 23 21:40:11 2009 +0100
@@ -70,7 +70,8 @@
   Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
   ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
   ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
-  ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML	\
+  ML-Systems/install_pp_polyml-experimental.ML				\
+  ML-Systems/use_context.ML Proof/extraction.ML				\
   Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
   Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML	\
   ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -46,6 +46,7 @@
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
 
 
 (*low-level pointer equality*)
@@ -120,7 +121,7 @@
 end;
 
 (*dummy implementation*)
-fun toplevel_pp _ _ _ _ _ = ();
+fun toplevel_pp _ _ _ = ();
 
 (*dummy implementation*)
 fun ml_prompts p1 p2 = ();
@@ -185,18 +186,18 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text (tune: string -> string) _ _ _ _ _ txt =
+fun use_text ({tune_source, ...}: use_context) _ _ txt =
   let
     val tmp_name = FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;
   in
-    TextIO.output (tmp_file, tune txt);
+    TextIO.output (tmp_file, tune_source txt);
     TextIO.closeOut tmp_file;
     use tmp_name;
     FileSys.remove tmp_name
   end;
 
-fun use_file _ _ _ _ _ name = use name;
+fun use_file _ _ name = use name;
 
 
 
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml-4.1.3.ML
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -6,6 +6,7 @@
 use "ML-Systems/polyml_old_basis.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml-4.1.4.ML
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -6,6 +6,7 @@
 use "ML-Systems/polyml_old_basis.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml-4.2.0.ML
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -5,6 +5,7 @@
 
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -5,6 +5,7 @@
 
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -4,6 +4,7 @@
 *)
 
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -4,6 +4,14 @@
 *)
 
 open Thread;
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+end;
+
 use "ML-Systems/polyml_common.ML";
 
 if ml_system = "polyml-5.2"
@@ -17,12 +25,6 @@
 
 (* runtime compilation *)
 
-structure ML_NameSpace =
-struct
-  open PolyML.NameSpace;
-  val global = PolyML.globalNameSpace;
-end;
-
 local
 
 fun drop_newline s =
@@ -31,11 +33,11 @@
 
 in
 
-fun use_text (tune: string -> string) str_of_pos
-    name_space (start_line, name) (print, err) verbose txt =
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+    (start_line, name) verbose txt =
   let
     val current_line = ref start_line;
-    val in_buffer = ref (String.explode (tune txt));
+    val in_buffer = ref (String.explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
@@ -58,14 +60,14 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
+        error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
 
 end;
 
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -9,8 +9,8 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/system_shell.ML";
-use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
 
 
 (** ML system and platform related **)
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml_old_compiler4.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -3,9 +3,9 @@
 Runtime compilation -- for old PolyML.compiler (version 4.x).
 *)
 
-fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt =
   let
-    val in_buffer = ref (explode (tune txt));
+    val in_buffer = ref (explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
@@ -21,12 +21,12 @@
       | _ => (PolyML.compiler (get, put) (); exec ()));
   in
     exec () handle exn =>
-      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+      (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml_old_compiler5.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -3,9 +3,9 @@
 Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
 *)
 
-fun use_text (tune: string -> string) _ _ (line, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   let
-    val in_buffer = ref (explode (tune txt));
+    val in_buffer = ref (explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
@@ -21,12 +21,12 @@
         [] => ()
       | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
   in
-    exec () handle exn => (err (output ()); raise exn);
+    exec () handle exn => (error (output ()); raise exn);
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/polyml_pp.ML
--- a/src/Pure/ML-Systems/polyml_pp.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_pp.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -14,7 +14,7 @@
       | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
   in pprint end;
 
-fun toplevel_pp tune str_of_pos output (_: string list) pp =
-  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context (_: string list) pp =
+  use_text context (1, "pp") false
     ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -14,6 +14,7 @@
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
 
 
 (*low-level pointer equality*)
@@ -100,7 +101,7 @@
 
 (* ML command execution *)
 
-fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   let
     val ref out_orig = Control.Print.out;
 
@@ -111,22 +112,20 @@
       in String.substring (str, 0, Int.max (0, size str - 1)) end;
   in
     Control.Print.out := out;
-    Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn =>
+    Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
       (Control.Print.out := out_orig;
-        err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+        error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     Control.Print.out := out_orig;
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
 
-fun forget_structure name =
-  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
-    ("structure " ^ name ^ " = struct end");
+fun forget_structure _ = ();
 
 
 (* toplevel pretty printing *)
@@ -143,8 +142,8 @@
       | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
   in pprint end;
 
-fun toplevel_pp tune str_of_pos output path pp =
-  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context path pp =
+  use_text context (1, "pp") false
     ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
       "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML-Systems/use_context.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/use_context.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -0,0 +1,13 @@
+(*  Title:      Pure/ML-Systems/use_context.ML
+    Author:     Makarius
+
+Common context for "use" operations (compiler invocation).
+*)
+
+type use_context =
+ {tune_source: string -> string,
+  name_space: ML_Name_Space.T,
+  str_of_pos: int -> string -> string,
+  print: string -> unit,
+  error: string -> unit};
+
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -20,7 +20,8 @@
   val the_local_context: unit -> Proof.context
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val inherit_env: Context.generic -> Context.generic -> Context.generic
-  val name_space: ML_NameSpace.nameSpace
+  val name_space: ML_Name_Space.T
+  val local_context: use_context
   val stored_thms: thm list ref
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
@@ -31,13 +32,10 @@
   val trace: bool ref
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
-  val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
-    Position.T -> Symbol_Pos.text -> unit
   val eval: bool -> Position.T -> Symbol_Pos.text -> unit
   val eval_file: Path.T -> unit
   val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
-  val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
-    string * (unit -> 'a) option ref -> string -> 'a
+  val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
   val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
 end
 
@@ -61,12 +59,12 @@
 structure ML_Env = GenericDataFun
 (
   type T =
-    ML_NameSpace.valueVal Symtab.table *
-    ML_NameSpace.typeVal Symtab.table *
-    ML_NameSpace.fixityVal Symtab.table *
-    ML_NameSpace.structureVal Symtab.table *
-    ML_NameSpace.signatureVal Symtab.table *
-    ML_NameSpace.functorVal Symtab.table;
+    ML_Name_Space.valueVal Symtab.table *
+    ML_Name_Space.typeVal Symtab.table *
+    ML_Name_Space.fixityVal Symtab.table *
+    ML_Name_Space.structureVal Symtab.table *
+    ML_Name_Space.signatureVal Symtab.table *
+    ML_Name_Space.functorVal Symtab.table;
   val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
   val extend = I;
   fun merge _
@@ -82,23 +80,23 @@
 
 val inherit_env = ML_Env.put o ML_Env.get;
 
-val name_space: ML_NameSpace.nameSpace =
+val name_space: ML_Name_Space.T =
   let
     fun lookup sel1 sel2 name =
       Context.thread_data ()
       |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
-      |> (fn NONE => sel2 ML_NameSpace.global name | some => some);
+      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
     fun all sel1 sel2 () =
       Context.thread_data ()
       |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
-      |> append (sel2 ML_NameSpace.global ())
+      |> append (sel2 ML_Name_Space.global ())
       |> sort_distinct (string_ord o pairself #1);
 
     fun enter ap1 sel2 entry =
       if is_some (Context.thread_data ()) then
         Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
-      else sel2 ML_NameSpace.global entry;
+      else sel2 ML_Name_Space.global entry;
   in
    {lookupVal    = lookup #1 #lookupVal,
     lookupType   = lookup #2 #lookupType,
@@ -120,6 +118,13 @@
     allFunct     = all #6 #allFunct}
   end;
 
+val local_context: use_context =
+ {tune_source = ML_Parse.fix_ints,
+  name_space = name_space,
+  str_of_pos = Position.str_of oo Position.line_file,
+  print = writeln,
+  error = error};
+
 
 (* theorem bindings *)
 
@@ -134,7 +139,7 @@
       else if not (ML_Syntax.is_identifier name) then
         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
       else setmp stored_thms ths' (fn () =>
-        use_text name_space (0, "") Output.ml_output true
+        use_text local_context (0, "") true
           ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
   in () end;
 
@@ -233,10 +238,10 @@
 
 val trace = ref false;
 
-fun eval_wrapper pr verbose pos txt =
+fun eval verbose pos txt =
   let
-    fun eval_raw p = use_text name_space
-      (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
+    fun eval_raw p = use_text local_context
+      (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
 
     (*prepare source text*)
     val _ = Position.report Markup.ML_source pos;
@@ -260,20 +265,18 @@
 end;
 
 
-(* ML evaluation *)
+(* derived versions *)
 
-val eval = eval_wrapper Output.ml_output;
 fun eval_file path = eval true (Path.position path) (File.read path);
 
 fun eval_in ctxt verbose pos txt =
   Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
 
-fun evaluate ctxt pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
+fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   let
     val _ = r := NONE;
     val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () =>
-      eval_wrapper pr verbose Position.none
-        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
+      eval verbose Position.none ("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 =
diff -r 2f64540707d6 -r beaadd5af500 src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -7,6 +7,7 @@
 signature ML_PARSE =
 sig
   val fix_ints: string -> string
+  val global_context: use_context
 end;
 
 structure ML_Parse: ML_PARSE =
@@ -62,4 +63,14 @@
 
 val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
 
+
+(* global use_context *)
+
+val global_context: use_context =
+ {tune_source = fix_ints,
+  name_space = ML_Name_Space.global,
+  str_of_pos = Position.str_of oo Position.line_file,
+  print = writeln,
+  error = error};
+
 end;
diff -r 2f64540707d6 -r beaadd5af500 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Tools/code/code_ml.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -969,7 +969,7 @@
         val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
-      in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
+      in ML_Context.evaluate ctxt false reff sml_code end;
   in eval'' thy (rpair eval') ct end;
 
 fun eval_term reff = eval Code_Thingol.eval_term I reff;
diff -r 2f64540707d6 -r beaadd5af500 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Mar 23 21:40:11 2009 +0100
+++ b/src/Tools/nbe.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -277,14 +277,12 @@
       in
         s
         |> tracing (fn s => "\n--- code to be evaluated:\n" ^ s)
-        |> ML_Context.evaluate ctxt
-            (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
-            Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
-            (!trace) univs_cookie
+        |> ML_Context.evaluate ctxt (!trace) univs_cookie
         |> (fn f => f deps_vals)
         |> (fn univs => cs ~~ univs)
       end;
 
+
 (* preparing function equations *)
 
 fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =