src/Pure/ML-Systems/smlnj.ML
changeset 30672 beaadd5af500
parent 30626 248de8dd839e
child 31321 fe786d4633b9
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 23 21:40:11 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 23 21:40:11 2009 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4  use "ML-Systems/system_shell.ML";
     1.5  use "ML-Systems/ml_name_space.ML";
     1.6  use "ML-Systems/ml_pretty.ML";
     1.7 +use "ML-Systems/use_context.ML";
     1.8  
     1.9  
    1.10  (*low-level pointer equality*)
    1.11 @@ -100,7 +101,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_source, print, error, ...}: use_context) (line, name) verbose txt =
    1.17    let
    1.18      val ref out_orig = Control.Print.out;
    1.19  
    1.20 @@ -111,22 +112,20 @@
    1.21        in String.substring (str, 0, Int.max (0, size str - 1)) end;
    1.22    in
    1.23      Control.Print.out := out;
    1.24 -    Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn =>
    1.25 +    Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
    1.26        (Control.Print.out := out_orig;
    1.27 -        err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.28 +        error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.29      Control.Print.out := out_orig;
    1.30      if verbose then print (output ()) else ()
    1.31    end;
    1.32  
    1.33 -fun use_file tune str_of_pos name_space output verbose name =
    1.34 +fun use_file context verbose name =
    1.35    let
    1.36      val instream = TextIO.openIn name;
    1.37      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.38 -  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
    1.39 +  in use_text context (1, name) verbose txt end;
    1.40  
    1.41 -fun forget_structure name =
    1.42 -  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
    1.43 -    ("structure " ^ name ^ " = struct end");
    1.44 +fun forget_structure _ = ();
    1.45  
    1.46  
    1.47  (* toplevel pretty printing *)
    1.48 @@ -143,8 +142,8 @@
    1.49        | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
    1.50    in pprint end;
    1.51  
    1.52 -fun toplevel_pp tune str_of_pos output path pp =
    1.53 -  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
    1.54 +fun toplevel_pp context path pp =
    1.55 +  use_text context (1, "pp") false
    1.56      ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
    1.57        "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
    1.58