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