# HG changeset patch # User wenzelm # Date 1285160022 -7200 # Node ID 507fcf86e1e0db32bff6f99d2afcdd9f8401fe82 # Parent f84b70e3bb9ca2e10078d6d4215672e3def86cec just one Session.raw_messages event bus; diff -r f84b70e3bb9c -r 507fcf86e1e0 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed Sep 22 14:29:13 2010 +0200 +++ b/src/Pure/System/session.scala Wed Sep 22 14:53:42 2010 +0200 @@ -41,8 +41,7 @@ /* pervasive event buses */ val global_settings = new Event_Bus[Session.Global_Settings.type] - val raw_protocol = new Event_Bus[Isabelle_Process.Result] - val raw_output = new Event_Bus[Isabelle_Process.Result] + val raw_messages = new Event_Bus[Isabelle_Process.Result] val commands_changed = new Event_Bus[Session.Commands_Changed] val perspective = new Event_Bus[Session.Perspective.type] val assignments = new Event_Bus[Session.Assignment.type] @@ -177,7 +176,7 @@ def handle_result(result: Isabelle_Process.Result) //{{{ { - raw_protocol.event(result) + raw_messages.event(result) result.properties match { case Position.Id(state_id) => @@ -202,8 +201,7 @@ } } else if (result.is_exit) prover = null // FIXME ?? - else if (result.is_stdout) raw_output.event(result) - else if (!result.is_system) bad_result(result) + else if (!result.is_system && !result.is_stdout) bad_result(result) } } //}}} diff -r f84b70e3bb9c -r 507fcf86e1e0 src/Tools/jEdit/src/jedit/protocol_dockable.scala --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed Sep 22 14:29:13 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed Sep 22 14:53:42 2010 +0200 @@ -34,6 +34,6 @@ } } - override def init() { Isabelle.session.raw_protocol += main_actor } - override def exit() { Isabelle.session.raw_protocol -= main_actor } + override def init() { Isabelle.session.raw_messages += main_actor } + override def exit() { Isabelle.session.raw_messages -= main_actor } } diff -r f84b70e3bb9c -r 507fcf86e1e0 src/Tools/jEdit/src/jedit/raw_output_dockable.scala --- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Wed Sep 22 14:29:13 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Wed Sep 22 14:53:42 2010 +0200 @@ -29,13 +29,14 @@ loop { react { case result: Isabelle_Process.Result => - Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } + if (result.is_stdout) + Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) } } } - override def init() { Isabelle.session.raw_output += main_actor } - override def exit() { Isabelle.session.raw_output -= main_actor } + override def init() { Isabelle.session.raw_messages += main_actor } + override def exit() { Isabelle.session.raw_messages -= main_actor } }