src/Pure/ML-Systems/smlnj.ML

 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.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";
 
 
 (*low-level pointer equality*)
 
 CM.autoload "$smlnj/init/init.cmi";

 fun makestring x = "dummy string for SML New Jersey";
 
 
 (* 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;
 
     val out_buffer = ref ([]: string list);
     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
     fun output () =
       let val str = implode (rev (! out_buffer))
       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;
-
-fun forget_structure name =
-  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
-    ("structure " ^ name ^ " = struct end");
+  in use_text context (1, name) verbose txt end;
+
+fun forget_structure _ = ();
 
 
 (* toplevel pretty printing *)
 
 fun ml_pprint pps =

       | pprint (ML_Pretty.String (s, _)) = str s
       | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
       | 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 ^ "))");