src/Pure/System/isabelle_process.scala
changeset 45633 2cb7e34f6096
parent 45158 db4bf4fb5492
child 45666 d83797ef0d2d
     1.1 --- a/src/Pure/System/isabelle_process.scala	Fri Nov 25 16:32:29 2011 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Nov 25 18:37:14 2011 +0100
     1.3 @@ -52,12 +52,13 @@
     1.4      def is_init = kind == Markup.INIT
     1.5      def is_exit = kind == Markup.EXIT
     1.6      def is_stdout = kind == Markup.STDOUT
     1.7 +    def is_stderr = kind == Markup.STDERR
     1.8      def is_system = kind == Markup.SYSTEM
     1.9      def is_status = kind == Markup.STATUS
    1.10      def is_report = kind == Markup.REPORT
    1.11      def is_raw = kind == Markup.RAW
    1.12      def is_ready = Isar_Document.is_ready(message)
    1.13 -    def is_syslog = is_init || is_exit || is_system || is_ready
    1.14 +    def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
    1.15  
    1.16      override def toString: String =
    1.17      {
    1.18 @@ -136,7 +137,7 @@
    1.19        val cmdline =
    1.20          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    1.21            (system_channel.isabelle_args ::: args)
    1.22 -      new Isabelle_System.Managed_Process(true, cmdline: _*)
    1.23 +      new Isabelle_System.Managed_Process(false, cmdline: _*)
    1.24      }
    1.25      catch { case e: IOException => system_channel.accepted(); throw(e) }
    1.26  
    1.27 @@ -181,13 +182,15 @@
    1.28        val (command_stream, message_stream) = system_channel.rendezvous()
    1.29  
    1.30        standard_input = stdin_actor()
    1.31 -      val stdout = stdout_actor()
    1.32 +      val stdout = raw_output_actor(false)
    1.33 +      val stderr = raw_output_actor(true)
    1.34        command_input = input_actor(command_stream)
    1.35        val message = message_actor(message_stream)
    1.36  
    1.37        val rc = process_result.join
    1.38        system_result("process terminated")
    1.39 -      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
    1.40 +      for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
    1.41 +        thread.join
    1.42        system_result("process_manager terminated")
    1.43        put_result(Markup.EXIT, "Return code: " + rc.toString)
    1.44      }
    1.45 @@ -238,11 +241,14 @@
    1.46    }
    1.47  
    1.48  
    1.49 -  /* raw stdout */
    1.50 +  /* raw output */
    1.51  
    1.52 -  private def stdout_actor(): (Thread, Actor) =
    1.53 +  private def raw_output_actor(err: Boolean): (Thread, Actor) =
    1.54    {
    1.55 -    val name = "standard_output"
    1.56 +    val (name, reader, markup) =
    1.57 +      if (err) ("standard_error", process.stderr, Markup.STDERR)
    1.58 +      else ("standard_output", process.stdout, Markup.STDOUT)
    1.59 +
    1.60      Simple_Thread.actor(name) {
    1.61        var result = new StringBuilder(100)
    1.62  
    1.63 @@ -252,17 +258,17 @@
    1.64            //{{{
    1.65            var c = -1
    1.66            var done = false
    1.67 -          while (!done && (result.length == 0 || process.stdout.ready)) {
    1.68 -            c = process.stdout.read
    1.69 +          while (!done && (result.length == 0 || reader.ready)) {
    1.70 +            c = reader.read
    1.71              if (c >= 0) result.append(c.asInstanceOf[Char])
    1.72              else done = true
    1.73            }
    1.74            if (result.length > 0) {
    1.75 -            put_result(Markup.STDOUT, result.toString)
    1.76 +            put_result(markup, result.toString)
    1.77              result.length = 0
    1.78            }
    1.79            else {
    1.80 -            process.stdout.close
    1.81 +            reader.close
    1.82              finished = true
    1.83            }
    1.84            //}}}