use_text/use_file now depend on explicit ML name space;

--- a/src/Pure/General/secure.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/General/secure.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -10,8 +10,10 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
-  val use_text: int * string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
-  val use_file: (string -> unit) * (string -> 'a) -> bool -> 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 commit: unit -> unit
   val system_out: string -> string * int
@@ -38,19 +40,19 @@
 
 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
 
-fun raw_use_text x = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) x;
-fun raw_use_file x = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) x;
+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 use_text pos pr verbose txt =
-  (secure_mltext (); raw_use_text pos pr verbose txt);
+fun use_text ns pos pr verbose txt =
+  (secure_mltext (); raw_use_text ns pos pr verbose txt);
 
-fun use_file pr verbose name =
-  (secure_mltext (); raw_use_file pr verbose name);
+fun use_file ns pr verbose name =
+  (secure_mltext (); raw_use_file ns pr verbose name);
 
-fun use name = use_file Output.ml_output true name;
+fun use name = use_file ML_NameSpace.global Output.ml_output true name;
 
 (*commit is dynamically bound!*)
-fun commit () = raw_use_text (0, "") Output.ml_output false "commit();";
+fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
 
 
 (* shell commands *)

--- a/src/Pure/ML-Systems/mosml.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -40,6 +40,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/ml_name_space.ML";
 
 
 (*low-level pointer equality*)
@@ -158,7 +159,7 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text (tune: string -> string) _ _ _ _ txt =
+fun use_text (tune: string -> string) _ _ _ _ _ txt =
   let
     val tmp_name = FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;
@@ -169,7 +170,7 @@
     FileSys.remove tmp_name
   end;
 
-fun use_file _ _ _ _ name = use name;
+fun use_file _ _ _ _ _ name = use name;
 
 
 

--- a/src/Pure/ML-Systems/polyml.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -13,6 +13,12 @@
 
 (* runtime compilation *)
 
+structure ML_NameSpace =
+struct
+  open PolyML.NameSpace;
+  val global = PolyML.globalNameSpace;
+end;
+
 local
 
 fun drop_newline s =
@@ -21,7 +27,8 @@
 
 in
 
-fun use_text (tune: string -> string) str_of_pos (start_line, name) (print, err) verbose txt =
+fun use_text (tune: string -> string) str_of_pos
+    name_space (start_line, name) (print, err) verbose txt =
   let
     val current_line = ref start_line;
     val in_buffer = ref (String.explode (tune txt));
@@ -40,7 +47,8 @@
     val parameters =
      [PolyML.Compiler.CPOutStream put,
       PolyML.Compiler.CPLineNo (fn () => ! current_line),
-      PolyML.Compiler.CPErrorMessageProc (put o message)];
+      PolyML.Compiler.CPErrorMessageProc (put o message),
+      PolyML.Compiler.CPNameSpace name_space];
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
@@ -49,10 +57,10 @@
         err (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-fun use_file tune str_of_pos output verbose name =
+fun use_file tune str_of_pos name_space output 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 (1, name) output verbose txt end;
+  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
 
 end;

--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -8,7 +8,7 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/system_shell.ML";
-
+use "ML-Systems/ml_name_space.ML";
 
 
 (** ML system and platform related **)

--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -4,7 +4,7 @@
 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: string -> string) _ _ (line: int, name) (print, err) verbose txt =
   let
     val in_buffer = ref (explode (tune txt));
     val out_buffer = ref ([]: string list);
@@ -26,9 +26,8 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos output verbose name =
+fun use_file tune str_of_pos name_space output 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 (1, name) output verbose txt end;
-
+  in use_text tune str_of_pos name_space (1, name) output verbose txt end;

--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -4,7 +4,7 @@
 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: string -> string) _ _ (line, name) (print, err) verbose txt =
   let
     val in_buffer = ref (explode (tune txt));
     val out_buffer = ref ([]: string list);
@@ -26,9 +26,8 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos output verbose name =
+fun use_file tune str_of_pos name_space output 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 (1, name) output verbose txt end;
-
+  in use_text tune str_of_pos name_space (1, name) output verbose txt end;

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -11,6 +11,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/system_shell.ML";
+use "ML-Systems/ml_name_space.ML";
 
 
 (*low-level pointer equality*)
@@ -112,7 +113,7 @@
 
 (* ML command execution *)
 
-fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
+fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
   let
     val ref out_orig = Control.Print.out;
 
@@ -130,11 +131,11 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos output verbose name =
+fun use_file tune str_of_pos name_space output 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 (1, name) output verbose txt end;
+  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

--- a/src/Tools/Compute_Oracle/am_compiler.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -186,7 +186,7 @@
 
     in
 	compiled_rewriter := NONE;	
-	use_text (1, "") Output.ml_output false (!buffer);
+	use_text ML_Context.name_space (1, "") Output.ml_output false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; r)

--- a/src/Tools/Compute_Oracle/am_sml.ML	Wed Sep 17 21:27:22 2008 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Wed Sep 17 21:27:24 2008 +0200
@@ -493,7 +493,7 @@
 
 fun writeTextFile name s = File.write (Path.explode name) s
 
-fun use_source src = use_text (1, "") Output.ml_output false src
+fun use_source src = use_text ML_Context.name_space (1, "") Output.ml_output false src
     
 fun compile cache_patterns const_arity eqs = 
     let