more specific message channels to avoid potential bottle-neck of raw_messages;
authorwenzelm
Tue Sep 06 11:25:27 2011 +0200 (2011-09-06)
changeset 447347313e2db3d39
parent 44733 329320fc88df
child 44735 66862d02678c
more specific message channels to avoid potential bottle-neck of raw_messages;
src/Pure/System/session.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/System/session.scala	Tue Sep 06 11:18:19 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Tue Sep 06 11:25:27 2011 +0200
     1.3 @@ -56,6 +56,8 @@
     1.4    val assignments = new Event_Bus[Session.Assignment.type]
     1.5    val commands_changed = new Event_Bus[Session.Commands_Changed]
     1.6    val phase_changed = new Event_Bus[Session.Phase]
     1.7 +  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
     1.8 +  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
     1.9    val raw_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
    1.10  
    1.11  
    1.12 @@ -451,6 +453,8 @@
    1.13  
    1.14              case result: Isabelle_Process.Result =>
    1.15                handle_result(result)
    1.16 +              if (result.is_syslog) syslog_messages.event(result)
    1.17 +              if (result.is_stdout) raw_output_messages.event(result)
    1.18                raw_messages.event(result)
    1.19            }
    1.20  
     2.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 11:18:19 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 11:25:27 2011 +0200
     2.3 @@ -29,8 +29,6 @@
     2.4    private val main_actor = actor {
     2.5      loop {
     2.6        react {
     2.7 -        case input: Isabelle_Process.Input =>
     2.8 -
     2.9          case result: Isabelle_Process.Result =>
    2.10            if (result.is_stdout)
    2.11              Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
    2.12 @@ -40,6 +38,6 @@
    2.13      }
    2.14    }
    2.15  
    2.16 -  override def init() { Isabelle.session.raw_messages += main_actor }
    2.17 -  override def exit() { Isabelle.session.raw_messages -= main_actor }
    2.18 +  override def init() { Isabelle.session.raw_output_messages += main_actor }
    2.19 +  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
    2.20  }
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 11:18:19 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 11:25:27 2011 +0200
     3.3 @@ -105,8 +105,6 @@
     3.4    private val main_actor = actor {
     3.5      loop {
     3.6        react {
     3.7 -        case input: Isabelle_Process.Input =>
     3.8 -
     3.9          case result: Isabelle_Process.Result =>
    3.10            if (result.is_syslog)
    3.11              Swing_Thread.now {
    3.12 @@ -127,13 +125,13 @@
    3.13    }
    3.14  
    3.15    override def init() {
    3.16 -    Isabelle.session.raw_messages += main_actor
    3.17 +    Isabelle.session.syslog_messages += main_actor
    3.18      Isabelle.session.phase_changed += main_actor
    3.19      Isabelle.session.commands_changed += main_actor
    3.20    }
    3.21  
    3.22    override def exit() {
    3.23 -    Isabelle.session.raw_messages -= main_actor
    3.24 +    Isabelle.session.syslog_messages -= main_actor
    3.25      Isabelle.session.phase_changed -= main_actor
    3.26      Isabelle.session.commands_changed -= main_actor
    3.27    }