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