# HG changeset patch
# User wenzelm
# Date 1329748608 -3600
# Node ID c54a4a22501cc94556545f4b5932b6d041a92ce3
# Parent  d1dcb91a512e08d8da33cd1fac778bd28c7644c9
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;

diff -r d1dcb91a512e -r c54a4a22501c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Feb 20 12:37:17 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Feb 20 15:36:48 2012 +0100
@@ -6,13 +6,13 @@
 
 Startup phases:
   . raw Posix process startup with uncontrolled output on stdout/stderr
-  . stdout \002: ML running
+  . stderr \002: ML running
   .. stdin/stdout/stderr freely available (raw ML loop)
   .. protocol thread initialization
   ... rendezvous on system channel
   ... message INIT(pid): channels ready
-  ... message STATUS(keywords)
-  ... message READY: main loop ready
+  ... message RAW(keywords)
+  ... message RAW(ready): main loop ready
 *)
 
 signature ISABELLE_PROCESS =
@@ -165,7 +165,7 @@
 fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
-    val _ = Output.physical_stdout Symbol.STX;
+    val _ = Output.physical_stderr Symbol.STX;
 
     val _ = quick_and_dirty := true;
     val _ = Goal.parallel_proofs := 0;
diff -r d1dcb91a512e -r c54a4a22501c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Feb 20 12:37:17 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Mon Feb 20 15:36:48 2012 +0100
@@ -152,15 +152,15 @@
 
   private val process_manager = Simple_Thread.fork("process_manager")
   {
-    val (startup_failed, startup_output) =
+    val (startup_failed, startup_errors) =
     {
       val expired = System.currentTimeMillis() + timeout.ms
       val result = new StringBuilder(100)
 
       var finished: Option[Boolean] = None
       while (finished.isEmpty && System.currentTimeMillis() <= expired) {
-        while (finished.isEmpty && process.stdout.ready) {
-          val c = process.stdout.read
+        while (finished.isEmpty && process.stderr.ready) {
+          val c = process.stderr.read
           if (c == 2) finished = Some(true)
           else result += c.toChar
         }
@@ -169,7 +169,7 @@
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
-    system_result(startup_output)
+    if (startup_errors != "") system_result(startup_errors)
 
     if (startup_failed) {
       put_result(Isabelle_Markup.EXIT, "Return code: 127")