src/Pure/ML-Systems/smlnj.ML
changeset 28268 ac8431ecd57e
parent 28151 61f9c918b410
child 28284 2161665a0a5d
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 21:27:22 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 21:27:24 2008 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  use "ML-Systems/thread_dummy.ML";
     1.5  use "ML-Systems/multithreading.ML";
     1.6  use "ML-Systems/system_shell.ML";
     1.7 +use "ML-Systems/ml_name_space.ML";
     1.8  
     1.9  
    1.10  (*low-level pointer equality*)
    1.11 @@ -112,7 +113,7 @@
    1.12  
    1.13  (* ML command execution *)
    1.14  
    1.15 -fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
    1.16 +fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
    1.17    let
    1.18      val ref out_orig = Control.Print.out;
    1.19  
    1.20 @@ -130,11 +131,11 @@
    1.21      if verbose then print (output ()) else ()
    1.22    end;
    1.23  
    1.24 -fun use_file tune str_of_pos output verbose name =
    1.25 +fun use_file tune str_of_pos name_space output verbose name =
    1.26    let
    1.27      val instream = TextIO.openIn name;
    1.28      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.29 -  in use_text tune str_of_pos (1, name) output verbose txt end;
    1.30 +  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
    1.31  
    1.32  fun forget_structure name =
    1.33    use_text (fn x => x) (fn _ => "") (1, "ML") (TextIO.print, fn s => raise Fail s) false