src/Tools/jEdit/src/raw_output_dockable.scala
changeset 45633 2cb7e34f6096
parent 44734 7313e2db3d39
child 46772 be21f050eda4
--- 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)