src/Pure/ML-Systems/smlnj.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5708 fb09ab6a447f
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -82,7 +82,21 @@
 
 (* ML command execution *)
 
-val use_text = Compiler.Interact.useStream o TextIO.openString;
+fun use_text verbose txt =
+  let
+    val ref out_orig = Compiler.Control.Print.out;
+
+    val out_buffer = ref ([]: string list);
+    val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
+
+    fun show_output () = print (implode (rev (! out_buffer)));
+  in
+    Compiler.Control.Print.out := out;
+    Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
+      (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
+    Compiler.Control.Print.out := out_orig;
+    if verbose then show_output () else ()
+  end;