# 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 }