# HG changeset patch
# User wenzelm
# Date 1334610460 -7200
# Node ID 4b0daca2bf889686d4fe1e812a3490065c3ebe2a
# Parent  e3fc50c7da136bb5b3395ca672eef15d1347aa89
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;

diff -r e3fc50c7da13 -r 4b0daca2bf88 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Apr 16 21:53:11 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Apr 16 23:07:40 2012 +0200
@@ -542,7 +542,7 @@
   | (output, _) =>
     error (case extract_known_failure known_perl_failures output of
              SOME failure => string_for_failure failure
-           | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
+           | NONE => trim_line output ^ ".")
 
 fun find_system name [] systems =
     find_first (String.isPrefix (name ^ "---")) systems
diff -r e3fc50c7da13 -r 4b0daca2bf88 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Mon Apr 16 21:53:11 2012 +0200
+++ b/src/Pure/Concurrent/bash.ML	Mon Apr 16 23:07:40 2012 +0200
@@ -6,7 +6,7 @@
 
 signature BASH =
 sig
-  val process: string -> {output: string, rc: int, terminate: unit -> unit}
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
 end;
 
 structure Bash: BASH =
@@ -19,7 +19,8 @@
 
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
-    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
     val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
 
     val system_thread =
@@ -31,8 +32,9 @@
               OS.Process.system
                 ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
                   File.shell_path pid_path ^ " script \"exec bash " ^
-                  File.shell_path script_path ^ " > " ^
-                  File.shell_path output_path ^ "\"");
+                  File.shell_path script_path ^
+                  " > " ^ File.shell_path out_path ^
+                  " 2> " ^ File.shell_path err_path ^ "\"");
             val res =
               (case Posix.Process.fromStatus status of
                 Posix.Process.W_EXITED => Result 0
@@ -75,7 +77,8 @@
     fun cleanup () =
      (Simple_Thread.interrupt_unsynchronized system_thread;
       try File.rm script_path;
-      try File.rm output_path;
+      try File.rm out_path;
+      try File.rm err_path;
       try File.rm pid_path);
   in
     let
@@ -83,11 +86,12 @@
         restore_attributes (fn () =>
           Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
 
-      val output = the_default "" (try File.read output_path);
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
       val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
       val pid = get_pid ();
       val _ = cleanup ();
-    in {output = output, rc = rc, terminate = fn () => terminate pid} end
+    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
     handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
   end);
 
diff -r e3fc50c7da13 -r 4b0daca2bf88 src/Pure/Concurrent/bash_sequential.ML
--- a/src/Pure/Concurrent/bash_sequential.ML	Mon Apr 16 21:53:11 2012 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML	Mon Apr 16 23:07:40 2012 +0200
@@ -7,7 +7,7 @@
 
 signature BASH =
 sig
-  val process: string -> {output: string, rc: int, terminate: unit -> unit}
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
 end;
 
 structure Bash: BASH =
@@ -17,16 +17,18 @@
   let
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
-    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
-    fun cleanup () = (try File.rm script_path; try File.rm output_path);
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+    fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path);
   in
     let
       val _ = File.write script_path script;
       val status =
         OS.Process.system
           ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
-            " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
-            File.shell_path output_path ^ "\"");
+            " script \"exec bash " ^ File.shell_path script_path ^
+            " > " ^ File.shell_path out_path ^
+            " 2> " ^ File.shell_path err_path ^ "\"");
       val rc =
         (case Posix.Process.fromStatus status of
           Posix.Process.W_EXITED => 0
@@ -34,9 +36,10 @@
         | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
         | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
 
-      val output = the_default "" (try File.read output_path);
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
       val _ = cleanup ();
-    in {output = output, rc = rc, terminate = fn () => ()} end
+    in {out = out, err = err, rc = rc, terminate = fn () => ()} end
     handle exn => (cleanup (); reraise exn)
   end;
 
diff -r e3fc50c7da13 -r 4b0daca2bf88 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Apr 16 21:53:11 2012 +0200
+++ b/src/Pure/System/isabelle_system.ML	Mon Apr 16 23:07:40 2012 +0200
@@ -25,13 +25,16 @@
 (* bash *)
 
 fun bash_output s =
-  let val {output, rc, ...} = Bash.process s
-  in (output, rc) end;
+  let
+    val {out, err, rc, ...} = Bash.process s;
+    val _ = warning (trim_line err);
+  in (out, rc) end;
 
 fun bash s =
-  (case bash_output s of
-    ("", rc) => rc
-  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+  let
+    val (out, rc) = bash_output s;
+    val _ = writeln (trim_line out);
+  in rc end;
 
 
 (* system commands *)
@@ -46,7 +49,7 @@
         else NONE
       end handle OS.SysErr _ => NONE) of
     SOME path => bash (File.shell_quote path ^ " " ^ args)
-  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
+  | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
 
 fun system_command cmd =
   if bash cmd <> 0 then error ("System command failed: " ^ cmd)
@@ -94,7 +97,7 @@
     (fn path =>
       (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
         (_, 0) => f path
-      | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
+      | (out, _) => error (trim_line out)));
 
 (* FIXME blocks on Cygwin 1.7.x *)
 (* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
@@ -104,7 +107,7 @@
       (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
         {rc = 0, terminate, ...} =>
           (restore_attributes f fifo handle exn => (terminate (); reraise exn))
-      | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ());
+      | {out, ...} => error (trim_line out))) ());
 
 end;
 
diff -r e3fc50c7da13 -r 4b0daca2bf88 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Apr 16 21:53:11 2012 +0200
+++ b/src/Pure/library.ML	Mon Apr 16 23:07:40 2012 +0200
@@ -150,6 +150,7 @@
   val suffix: string -> string -> string
   val unprefix: string -> string -> string
   val unsuffix: string -> string -> string
+  val trim_line: string -> string
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
   val match_string: string -> string -> bool
@@ -755,6 +756,8 @@
   if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   else raise Fail "unsuffix";
 
+val trim_line = perhaps (try (unsuffix "\n"));
+
 fun replicate_string (0: int) _ = ""
   | replicate_string 1 a = a
   | replicate_string k a =