use_text: verbose flag;

--- a/src/Pure/ML-Systems/mlworks.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -66,7 +66,7 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text txt =
+fun use_text _ txt =
   let
     val tmp_name = OS.FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;

--- a/src/Pure/ML-Systems/polyml.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -41,18 +41,27 @@
 
 (* ML command execution -- 'eval' *)
 
-fun use_text txt =
+fun use_text verbose txt =
   let
-    val buffer = ref (explode txt);
+    val in_buffer = ref (explode txt);
+    val out_buffer = ref ([]: string list);
+
     fun get () =
-      (case ! buffer of
+      (case ! in_buffer of
         [] => ""
-      | c :: cs => (buffer := cs; c));
+      | c :: cs => (in_buffer := cs; c));
+    fun put s = out_buffer := s :: ! out_buffer;
+
     fun exec () =
-      (case ! buffer of
+      (case ! in_buffer of
         [] => ()
-      | _ => (PolyML.compiler (get, print) (); exec ()));
-  in exec () end;
+      | _ => (PolyML.compiler (get, put) (); exec ()));
+
+    fun show_output () = print (implode (rev (! out_buffer)));
+  in
+    exec () handle exn => (show_output (); raise exn);
+    if verbose then show_output () else ()
+  end;
 
 
 

--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -81,7 +81,7 @@
 
 (* ML command execution *)
 
-val use_text = System.Compile.use_stream o open_string;
+fun use_text _ = System.Compile.use_stream o open_string;
 
 
 

--- 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;
 
 
 

--- a/src/Pure/Thy/thm_database.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -52,7 +52,7 @@
   let val thm' = store_thm (name, thm) in
     if is_ml_identifier name then
       (qed_thm := Some thm';
-        use_text ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
+        use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
     else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
   end;
 

--- a/src/Pure/Thy/thy_read.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/Thy/thy_read.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -267,7 +267,7 @@
              Use.use ml_file);
 
        (*Store theory again because it could have been redefined*)
-       use_text ("val _ = store_theory " ^ tname ^ ".thy;");
+       use_text false ("val _ = store_theory " ^ tname ^ ".thy;");
 
        (*Add theory to list of all loaded theories (for index.html)
          and add it to its parents' sub-charts*)