src/Pure/ML-Systems/smlnj.ML
changeset 22144 c33450acd873
parent 21770 ea6f846d8c4b
child 23139 aa899bce7c3b
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Jan 21 13:27:41 2007 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun Jan 21 16:43:42 2007 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  
     1.5  (* ML command execution *)
     1.6  
     1.7 -fun use_text (print, err) verbose txt =
     1.8 +fun use_text name (print, err) verbose txt =
     1.9    let
    1.10      val ref out_orig = Control.Print.out;
    1.11  
    1.12 @@ -108,7 +108,8 @@
    1.13    in
    1.14      Control.Print.out := out;
    1.15      Backend.Interact.useStream (TextIO.openString txt) handle exn =>
    1.16 -      (Control.Print.out := out_orig; err (output ()); raise exn);
    1.17 +      (Control.Print.out := out_orig;
    1.18 +        err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.19      Control.Print.out := out_orig;
    1.20      if verbose then print (output ()) else ()
    1.21    end;