use_text: added name argument;

--- a/src/Pure/General/secure.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/General/secure.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -10,7 +10,7 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
-  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
+  val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
   val commit: unit -> unit
@@ -40,12 +40,12 @@
 val orig_use_text = use_text;
 val orig_use_file = use_file;
 
-fun use_text pr verbose txt = (secure_mltext (); orig_use_text pr verbose txt);
+fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt);
 fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
 val use = use_file Output.ml_output true;
 
 (*commit is dynamically bound!*)
-fun commit () = orig_use_text Output.ml_output false "commit();";
+fun commit () = orig_use_text "" Output.ml_output false "commit();";
 
 
 (* shell commands *)

--- a/src/Pure/ML-Systems/mosml.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -133,7 +133,7 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text _ _ txt =
+fun use_text _ _ _ txt =
   let
     val tmp_name = FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;

--- a/src/Pure/ML-Systems/polyml-5.0.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -12,9 +12,7 @@
 
 (* improved versions of use_text/file *)
 
-local
-
-fun use_ml name (print, err) verbose txt =
+fun use_text name (print, err) verbose txt =
   let
     val in_buffer = ref (explode txt);
     val out_buffer = ref ([]: string list);
@@ -37,14 +35,8 @@
     if verbose then print (output ()) else ()
   end;
 
-in
-
-fun use_text output = use_ml "ML text" output;
-
 fun use_file output verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_ml name output verbose txt end;
-
-end;
+  in use_text name output verbose txt end;

--- a/src/Pure/ML-Systems/polyml.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -90,7 +90,7 @@
 
 (* ML command execution -- 'eval' *)
 
-fun use_text (print, err) verbose txt =
+fun use_text name (print, err) verbose txt =
   let
     val in_buffer = ref (explode txt);
     val out_buffer = ref ([]: string list);
@@ -107,7 +107,8 @@
         [] => ()
       | _ => (PolyML.compiler (get, put) (); exec ()));
   in
-    exec () handle exn => (err (output ()); raise exn);
+    exec () handle exn =>
+      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     if verbose then print (output ()) else ()
   end;
 
@@ -119,7 +120,7 @@
   fun println s =
     (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
   fun eval "-q" = ()
-    | eval txt = use_text (println, println) false txt;
+    | eval txt = use_text "" (println, println) false txt;
 in
   val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
 end;

--- a/src/Pure/ML-Systems/poplogml.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -377,5 +377,5 @@
 
 end;
 
-fun use_text _ _ txt = use_string txt;
+fun use_text _ _ _ txt = use_string txt;
 fun use_file _ _ name = use name;

--- a/src/Pure/ML-Systems/smlnj.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -96,7 +96,7 @@
 
 (* ML command execution *)
 
-fun use_text (print, err) verbose txt =
+fun use_text name (print, err) verbose txt =
   let
     val ref out_orig = Control.Print.out;
 
@@ -108,7 +108,8 @@
   in
     Control.Print.out := out;
     Backend.Interact.useStream (TextIO.openString txt) handle exn =>
-      (Control.Print.out := out_orig; err (output ()); raise exn);
+      (Control.Print.out := out_orig;
+        err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     Control.Print.out := out_orig;
     if verbose then print (output ()) else ()
   end;

--- a/src/Pure/Thy/thm_database.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/Thy/thm_database.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -46,7 +46,7 @@
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
-val use_text_verbose = use_text Output.ml_output true;
+val use_text_verbose = use_text "" Output.ml_output true;
 
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in

--- a/src/Pure/Tools/am_compiler.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/Tools/am_compiler.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -216,7 +216,7 @@
 	    end
     in
 	compiled_rewriter := NONE;	
-	use_text (K (), K ()) false (!buffer);
+	use_text "" Output.ml_output false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))

--- a/src/Pure/Tools/codegen_serializer.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -1024,7 +1024,7 @@
   let
     fun output_file file = File.write (Path.explode file) o code_output;
     val output_diag = writeln o code_output;
-    val output_internal = use_text Output.ml_output false o code_output;
+    val output_internal = use_text "" Output.ml_output false o code_output;
   in
     parse_args ((Args.$$$ "-" >> K output_diag
       || Args.$$$ "#" >> K output_internal
@@ -1592,7 +1592,7 @@
     fun eval p = (
       reff := NONE;
       if !eval_verbose then Pretty.writeln p else ();
-      use_text Output.ml_output (!eval_verbose)
+      use_text "" Output.ml_output (!eval_verbose)
         ((Pretty.output o Pretty.chunks) [p,
           str ("val _ = (" ^ ref_name ^ " := SOME " ^ val_name' ^ ")")
         ]);

--- a/src/Pure/Tools/nbe.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/Tools/nbe.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -115,7 +115,7 @@
     fun use_code NONE = ()
       | use_code (SOME s) =
           (tracing (fn () => "\n---generated code:\n" ^ s) ();
-           use_text (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
+           use_text "" (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
                 Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
             (!trace) s);
 

--- a/src/Pure/codegen.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/codegen.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -991,7 +991,7 @@
                   [Pretty.str "]"])]],
             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = use_text Output.ml_output false s;
+    val _ = use_text "" Output.ml_output false s;
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (warning "Exception Match raised in generated code"; NONE)) of
@@ -1043,7 +1043,7 @@
             [Pretty.str "result"],
           Pretty.str ";"])  ^
       "\n\nend;\n";
-    val _ = use_text Output.ml_output false s
+    val _ = use_text "" Output.ml_output false s
   in !eval_result end);
 
 fun print_evaluated_term s = Toplevel.keep (fn state =>
@@ -1150,7 +1150,7 @@
        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
-         NONE => use_text Output.ml_output false
+         NONE => use_text "" Output.ml_output false
            (space_implode "\n" (map snd code))
        | SOME fname =>
            if lib then