--- a/src/Tools/jEdit/src/jedit/session_dockable.scala Thu Sep 23 14:26:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Thu Sep 23 14:39:29 2010 +0200
@@ -53,8 +53,10 @@
loop {
react {
case result: Isabelle_Process.Result =>
- if (result.is_init || result.is_exit || result.is_system || result.is_ready)
- Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") }
+ if (result.is_syslog)
+ Swing_Thread.now {
+ syslog.append(XML.content(result.message).mkString + "\n")
+ }
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
}