clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
--- 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;
--- 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")