# HG changeset patch
# User wenzelm
# Date 1315301127 -7200
# Node ID 7313e2db3d398c18bdc80c3e4c30215ad37a86f5
# Parent  329320fc88df5de8f4af2c50b026e1472964b9aa
more specific message channels to avoid potential bottle-neck of raw_messages;

diff -r 329320fc88df -r 7313e2db3d39 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Sep 06 11:18:19 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Sep 06 11:25:27 2011 +0200
@@ -56,6 +56,8 @@
   val assignments = new Event_Bus[Session.Assignment.type]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val phase_changed = new Event_Bus[Session.Phase]
+  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
+  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
   val raw_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
 
 
@@ -451,6 +453,8 @@
 
             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)
               raw_messages.event(result)
           }
 
diff -r 329320fc88df -r 7313e2db3d39 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 11:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 11:25:27 2011 +0200
@@ -29,8 +29,6 @@
   private val main_actor = actor {
     loop {
       react {
-        case input: Isabelle_Process.Input =>
-
         case result: Isabelle_Process.Result =>
           if (result.is_stdout)
             Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
@@ -40,6 +38,6 @@
     }
   }
 
-  override def init() { Isabelle.session.raw_messages += main_actor }
-  override def exit() { Isabelle.session.raw_messages -= main_actor }
+  override def init() { Isabelle.session.raw_output_messages += main_actor }
+  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
 }
diff -r 329320fc88df -r 7313e2db3d39 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 11:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 11:25:27 2011 +0200
@@ -105,8 +105,6 @@
   private val main_actor = actor {
     loop {
       react {
-        case input: Isabelle_Process.Input =>
-
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {
@@ -127,13 +125,13 @@
   }
 
   override def init() {
-    Isabelle.session.raw_messages += main_actor
+    Isabelle.session.syslog_messages += main_actor
     Isabelle.session.phase_changed += main_actor
     Isabelle.session.commands_changed += main_actor
   }
 
   override def exit() {
-    Isabelle.session.raw_messages -= main_actor
+    Isabelle.session.syslog_messages -= main_actor
     Isabelle.session.phase_changed -= main_actor
     Isabelle.session.commands_changed -= main_actor
   }