# HG changeset patch
# User wenzelm
# Date 1322242634 -3600
# Node ID 2cb7e34f6096b385c3e59dc98990162e48bd8b62
# Parent  b23c42b9f78a5bf8aa7222decab5518cfd60bda0
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

diff -r b23c42b9f78a -r 2cb7e34f6096 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Nov 25 16:32:29 2011 +0100
+++ b/src/Pure/General/markup.scala	Fri Nov 25 18:37:14 2011 +0100
@@ -257,6 +257,7 @@
   val RAW = "raw"
   val SYSTEM = "system"
   val STDOUT = "stdout"
+  val STDERR = "stderr"
   val EXIT = "exit"
 
   val LEGACY = "legacy"
diff -r b23c42b9f78a -r 2cb7e34f6096 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Nov 25 16:32:29 2011 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Nov 25 18:37:14 2011 +0100
@@ -52,12 +52,13 @@
     def is_init = kind == Markup.INIT
     def is_exit = kind == Markup.EXIT
     def is_stdout = kind == Markup.STDOUT
+    def is_stderr = kind == Markup.STDERR
     def is_system = kind == Markup.SYSTEM
     def is_status = kind == Markup.STATUS
     def is_report = kind == Markup.REPORT
     def is_raw = kind == Markup.RAW
     def is_ready = Isar_Document.is_ready(message)
-    def is_syslog = is_init || is_exit || is_system || is_ready
+    def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
 
     override def toString: String =
     {
@@ -136,7 +137,7 @@
       val cmdline =
         Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
           (system_channel.isabelle_args ::: args)
-      new Isabelle_System.Managed_Process(true, cmdline: _*)
+      new Isabelle_System.Managed_Process(false, cmdline: _*)
     }
     catch { case e: IOException => system_channel.accepted(); throw(e) }
 
@@ -181,13 +182,15 @@
       val (command_stream, message_stream) = system_channel.rendezvous()
 
       standard_input = stdin_actor()
-      val stdout = stdout_actor()
+      val stdout = raw_output_actor(false)
+      val stderr = raw_output_actor(true)
       command_input = input_actor(command_stream)
       val message = message_actor(message_stream)
 
       val rc = process_result.join
       system_result("process terminated")
-      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
+      for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
+        thread.join
       system_result("process_manager terminated")
       put_result(Markup.EXIT, "Return code: " + rc.toString)
     }
@@ -238,11 +241,14 @@
   }
 
 
-  /* raw stdout */
+  /* raw output */
 
-  private def stdout_actor(): (Thread, Actor) =
+  private def raw_output_actor(err: Boolean): (Thread, Actor) =
   {
-    val name = "standard_output"
+    val (name, reader, markup) =
+      if (err) ("standard_error", process.stderr, Markup.STDERR)
+      else ("standard_output", process.stdout, Markup.STDOUT)
+
     Simple_Thread.actor(name) {
       var result = new StringBuilder(100)
 
@@ -252,17 +258,17 @@
           //{{{
           var c = -1
           var done = false
-          while (!done && (result.length == 0 || process.stdout.ready)) {
-            c = process.stdout.read
+          while (!done && (result.length == 0 || reader.ready)) {
+            c = reader.read
             if (c >= 0) result.append(c.asInstanceOf[Char])
             else done = true
           }
           if (result.length > 0) {
-            put_result(Markup.STDOUT, result.toString)
+            put_result(markup, result.toString)
             result.length = 0
           }
           else {
-            process.stdout.close
+            reader.close
             finished = true
           }
           //}}}
diff -r b23c42b9f78a -r 2cb7e34f6096 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Nov 25 16:32:29 2011 +0100
+++ b/src/Pure/System/session.scala	Fri Nov 25 18:37:14 2011 +0100
@@ -455,7 +455,7 @@
             case result: Isabelle_Process.Result =>
               handle_result(result)
               if (result.is_syslog) syslog_messages.event(result)
-              if (result.is_stdout) raw_output_messages.event(result)
+              if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
               raw_messages.event(result)
           }
 
diff -r b23c42b9f78a -r 2cb7e34f6096 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Nov 25 16:32:29 2011 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Nov 25 18:37:14 2011 +0100
@@ -30,7 +30,7 @@
     loop {
       react {
         case result: Isabelle_Process.Result =>
-          if (result.is_stdout)
+          if (result.is_stdout || result.is_stderr)
             Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)