retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
authorwenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 456332cb7e34f6096
parent 45632 b23c42b9f78a
child 45634 b3dce535960f
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
src/Pure/General/markup.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/raw_output_dockable.scala
     1.1 --- a/src/Pure/General/markup.scala	Fri Nov 25 16:32:29 2011 +0100
     1.2 +++ b/src/Pure/General/markup.scala	Fri Nov 25 18:37:14 2011 +0100
     1.3 @@ -257,6 +257,7 @@
     1.4    val RAW = "raw"
     1.5    val SYSTEM = "system"
     1.6    val STDOUT = "stdout"
     1.7 +  val STDERR = "stderr"
     1.8    val EXIT = "exit"
     1.9  
    1.10    val LEGACY = "legacy"
     2.1 --- a/src/Pure/System/isabelle_process.scala	Fri Nov 25 16:32:29 2011 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Nov 25 18:37:14 2011 +0100
     2.3 @@ -52,12 +52,13 @@
     2.4      def is_init = kind == Markup.INIT
     2.5      def is_exit = kind == Markup.EXIT
     2.6      def is_stdout = kind == Markup.STDOUT
     2.7 +    def is_stderr = kind == Markup.STDERR
     2.8      def is_system = kind == Markup.SYSTEM
     2.9      def is_status = kind == Markup.STATUS
    2.10      def is_report = kind == Markup.REPORT
    2.11      def is_raw = kind == Markup.RAW
    2.12      def is_ready = Isar_Document.is_ready(message)
    2.13 -    def is_syslog = is_init || is_exit || is_system || is_ready
    2.14 +    def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
    2.15  
    2.16      override def toString: String =
    2.17      {
    2.18 @@ -136,7 +137,7 @@
    2.19        val cmdline =
    2.20          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    2.21            (system_channel.isabelle_args ::: args)
    2.22 -      new Isabelle_System.Managed_Process(true, cmdline: _*)
    2.23 +      new Isabelle_System.Managed_Process(false, cmdline: _*)
    2.24      }
    2.25      catch { case e: IOException => system_channel.accepted(); throw(e) }
    2.26  
    2.27 @@ -181,13 +182,15 @@
    2.28        val (command_stream, message_stream) = system_channel.rendezvous()
    2.29  
    2.30        standard_input = stdin_actor()
    2.31 -      val stdout = stdout_actor()
    2.32 +      val stdout = raw_output_actor(false)
    2.33 +      val stderr = raw_output_actor(true)
    2.34        command_input = input_actor(command_stream)
    2.35        val message = message_actor(message_stream)
    2.36  
    2.37        val rc = process_result.join
    2.38        system_result("process terminated")
    2.39 -      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
    2.40 +      for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
    2.41 +        thread.join
    2.42        system_result("process_manager terminated")
    2.43        put_result(Markup.EXIT, "Return code: " + rc.toString)
    2.44      }
    2.45 @@ -238,11 +241,14 @@
    2.46    }
    2.47  
    2.48  
    2.49 -  /* raw stdout */
    2.50 +  /* raw output */
    2.51  
    2.52 -  private def stdout_actor(): (Thread, Actor) =
    2.53 +  private def raw_output_actor(err: Boolean): (Thread, Actor) =
    2.54    {
    2.55 -    val name = "standard_output"
    2.56 +    val (name, reader, markup) =
    2.57 +      if (err) ("standard_error", process.stderr, Markup.STDERR)
    2.58 +      else ("standard_output", process.stdout, Markup.STDOUT)
    2.59 +
    2.60      Simple_Thread.actor(name) {
    2.61        var result = new StringBuilder(100)
    2.62  
    2.63 @@ -252,17 +258,17 @@
    2.64            //{{{
    2.65            var c = -1
    2.66            var done = false
    2.67 -          while (!done && (result.length == 0 || process.stdout.ready)) {
    2.68 -            c = process.stdout.read
    2.69 +          while (!done && (result.length == 0 || reader.ready)) {
    2.70 +            c = reader.read
    2.71              if (c >= 0) result.append(c.asInstanceOf[Char])
    2.72              else done = true
    2.73            }
    2.74            if (result.length > 0) {
    2.75 -            put_result(Markup.STDOUT, result.toString)
    2.76 +            put_result(markup, result.toString)
    2.77              result.length = 0
    2.78            }
    2.79            else {
    2.80 -            process.stdout.close
    2.81 +            reader.close
    2.82              finished = true
    2.83            }
    2.84            //}}}
     3.1 --- a/src/Pure/System/session.scala	Fri Nov 25 16:32:29 2011 +0100
     3.2 +++ b/src/Pure/System/session.scala	Fri Nov 25 18:37:14 2011 +0100
     3.3 @@ -455,7 +455,7 @@
     3.4              case result: Isabelle_Process.Result =>
     3.5                handle_result(result)
     3.6                if (result.is_syslog) syslog_messages.event(result)
     3.7 -              if (result.is_stdout) raw_output_messages.event(result)
     3.8 +              if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
     3.9                raw_messages.event(result)
    3.10            }
    3.11  
     4.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Nov 25 16:32:29 2011 +0100
     4.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Nov 25 18:37:14 2011 +0100
     4.3 @@ -30,7 +30,7 @@
     4.4      loop {
     4.5        react {
     4.6          case result: Isabelle_Process.Result =>
     4.7 -          if (result.is_stdout)
     4.8 +          if (result.is_stdout || result.is_stderr)
     4.9              Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
    4.10  
    4.11          case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)