clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
authorwenzelm
Mon Feb 20 15:36:48 2012 +0100 (2012-02-20 ago)
changeset 46548c54a4a22501c
parent 46547 d1dcb91a512e
child 46549 1bffe63879af
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/System/isabelle_process.ML	Mon Feb 20 12:37:17 2012 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Feb 20 15:36:48 2012 +0100
     1.3 @@ -6,13 +6,13 @@
     1.4  
     1.5  Startup phases:
     1.6    . raw Posix process startup with uncontrolled output on stdout/stderr
     1.7 -  . stdout \002: ML running
     1.8 +  . stderr \002: ML running
     1.9    .. stdin/stdout/stderr freely available (raw ML loop)
    1.10    .. protocol thread initialization
    1.11    ... rendezvous on system channel
    1.12    ... message INIT(pid): channels ready
    1.13 -  ... message STATUS(keywords)
    1.14 -  ... message READY: main loop ready
    1.15 +  ... message RAW(keywords)
    1.16 +  ... message RAW(ready): main loop ready
    1.17  *)
    1.18  
    1.19  signature ISABELLE_PROCESS =
    1.20 @@ -165,7 +165,7 @@
    1.21  fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
    1.22    let
    1.23      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
    1.24 -    val _ = Output.physical_stdout Symbol.STX;
    1.25 +    val _ = Output.physical_stderr Symbol.STX;
    1.26  
    1.27      val _ = quick_and_dirty := true;
    1.28      val _ = Goal.parallel_proofs := 0;
     2.1 --- a/src/Pure/System/isabelle_process.scala	Mon Feb 20 12:37:17 2012 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Feb 20 15:36:48 2012 +0100
     2.3 @@ -152,15 +152,15 @@
     2.4  
     2.5    private val process_manager = Simple_Thread.fork("process_manager")
     2.6    {
     2.7 -    val (startup_failed, startup_output) =
     2.8 +    val (startup_failed, startup_errors) =
     2.9      {
    2.10        val expired = System.currentTimeMillis() + timeout.ms
    2.11        val result = new StringBuilder(100)
    2.12  
    2.13        var finished: Option[Boolean] = None
    2.14        while (finished.isEmpty && System.currentTimeMillis() <= expired) {
    2.15 -        while (finished.isEmpty && process.stdout.ready) {
    2.16 -          val c = process.stdout.read
    2.17 +        while (finished.isEmpty && process.stderr.ready) {
    2.18 +          val c = process.stderr.read
    2.19            if (c == 2) finished = Some(true)
    2.20            else result += c.toChar
    2.21          }
    2.22 @@ -169,7 +169,7 @@
    2.23        }
    2.24        (finished.isEmpty || !finished.get, result.toString.trim)
    2.25      }
    2.26 -    system_result(startup_output)
    2.27 +    if (startup_errors != "") system_result(startup_errors)
    2.28  
    2.29      if (startup_failed) {
    2.30        put_result(Isabelle_Markup.EXIT, "Return code: 127")