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