# HG changeset patch # User wenzelm # Date 1281896849 -7200 # Node ID a9cff3f2e47923fc9195e273df73797264ab1837 # Parent f96394dba33586140db7d0068db9797e907e4bd2 renamed raw_results to raw_protocol; diff -r f96394dba335 -r a9cff3f2e479 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sun Aug 15 20:19:56 2010 +0200 +++ b/src/Pure/System/session.scala Sun Aug 15 20:27:29 2010 +0200 @@ -40,7 +40,7 @@ /* pervasive event buses */ val global_settings = new Event_Bus[Session.Global_Settings.type] - val raw_results = new Event_Bus[Isabelle_Process.Result] + val raw_protocol = new Event_Bus[Isabelle_Process.Result] val raw_output = new Event_Bus[Isabelle_Process.Result] val commands_changed = new Event_Bus[Session.Commands_Changed] val perspective = new Event_Bus[Session.Perspective.type] @@ -129,7 +129,7 @@ def handle_result(result: Isabelle_Process.Result) //{{{ { - raw_results.event(result) + raw_protocol.event(result) Position.get_id(result.properties) match { case Some(state_id) => diff -r f96394dba335 -r a9cff3f2e479 src/Tools/jEdit/src/jedit/protocol_dockable.scala --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Sun Aug 15 20:19:56 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Sun Aug 15 20:27:29 2010 +0200 @@ -34,6 +34,6 @@ } } - override def init() { Isabelle.session.raw_results += main_actor } - override def exit() { Isabelle.session.raw_results -= main_actor } + override def init() { Isabelle.session.raw_protocol += main_actor } + override def exit() { Isabelle.session.raw_protocol -= main_actor } }