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