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)