separate event bus and dockable for raw output (stdout);

--- a/src/Pure/System/session.scala	Sat May 22 20:37:59 2010 +0200
+++ b/src/Pure/System/session.scala	Sat May 22 20:59:55 2010 +0200
@@ -36,6 +36,7 @@
 
   val global_settings = new Event_Bus[Session.Global_Settings.type]
   val raw_results = new Event_Bus[Isabelle_Process.Result]
+  val raw_output = new Event_Bus[Isabelle_Process.Result]
   val results = new Event_Bus[Command]
 
   val command_change = new Event_Bus[Command]
@@ -148,6 +149,8 @@
       }
       else if (result.kind == Isabelle_Process.Kind.EXIT)
         prover = null
+      else if (result.is_raw)
+        raw_output.event(result)
       else if (!result.is_system)   // FIXME syslog (!?)
         bad_result(result)
     }

--- a/src/Tools/jEdit/plugin/Isabelle.props	Sat May 22 20:37:59 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Sat May 22 20:59:55 2010 +0200
@@ -31,13 +31,15 @@
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-raw-output isabelle.show-protocol
 isabelle.activate.label=Activate current buffer
 isabelle.show-output.label=Show Output
+isabelle.show-raw-output.label=Show Raw Output
 isabelle.show-protocol.label=Show Protocol
 
 #dockables
 isabelle-output.title=Output
+isabelle-raw-output.title=Raw Output
 isabelle-protocol.title=Protocol
 
 #SideKick

--- a/src/Tools/jEdit/plugin/actions.xml	Sat May 22 20:37:59 2010 +0200
+++ b/src/Tools/jEdit/plugin/actions.xml	Sat May 22 20:59:55 2010 +0200
@@ -15,6 +15,11 @@
 			wm.addDockableWindow("isabelle-output");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.show-raw-output">
+		<CODE>
+			wm.addDockableWindow("isabelle-raw-output");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.show-protocol">
 		<CODE>
 			wm.addDockableWindow("isabelle-protocol");

--- a/src/Tools/jEdit/plugin/dockables.xml	Sat May 22 20:37:59 2010 +0200
+++ b/src/Tools/jEdit/plugin/dockables.xml	Sat May 22 20:59:55 2010 +0200
@@ -5,6 +5,9 @@
 	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
 		new isabelle.jedit.Output_Dockable(view, position);
 	</DOCKABLE>
+	<DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+		new isabelle.jedit.Raw_Output_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
 		new isabelle.jedit.Protocol_Dockable(view, position);
 	</DOCKABLE>

--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Sat May 22 20:37:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Sat May 22 20:59:55 2010 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/jedit/protocol_dockable.scala
     Author:     Makarius
 
-Dockable window for raw process output.
+Dockable window for raw protocol messages.
 */
 
 package isabelle.jedit
@@ -29,13 +29,13 @@
 
   /* actor wiring */
 
-  private val raw_actor = actor {
+  private val protocol_actor = actor {
     loop {
       react {
         case result: Isabelle_Process.Result =>
           Swing_Thread.now { text_area.append(result.message.toString + "\n") }
 
-        case bad => System.err.println("raw_actor: ignoring bad message " + bad)
+        case bad => System.err.println("protocol_actor: ignoring bad message " + bad)
       }
     }
   }
@@ -43,12 +43,12 @@
   override def addNotify()
   {
     super.addNotify()
-    Isabelle.session.raw_results += raw_actor
+    Isabelle.session.raw_results += protocol_actor
   }
 
   override def removeNotify()
   {
-    Isabelle.session.raw_results -= raw_actor
+    Isabelle.session.raw_results -= protocol_actor
     super.removeNotify()
   }
 }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat May 22 20:59:55 2010 +0200
@@ -0,0 +1,54 @@
+/*  Title:      Tools/jEdit/src/jedit/raw_output_dockable.scala
+    Author:     Makarius
+
+Dockable window for raw process output (stdout).
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import java.awt.{Dimension, Graphics, BorderLayout}
+import javax.swing.{JPanel, JTextArea, JScrollPane}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class Raw_Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+{
+  if (position == DockableWindowManager.FLOATING)
+    setPreferredSize(new Dimension(500, 250))
+
+  private val text_area = new JTextArea
+  add(new JScrollPane(text_area), BorderLayout.CENTER)
+
+
+  /* actor wiring */
+
+  private val raw_output_actor = actor {
+    loop {
+      react {
+        case result: Isabelle_Process.Result =>
+          Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
+
+        case bad => System.err.println("raw_output_actor: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def addNotify()
+  {
+    super.addNotify()
+    Isabelle.session.raw_output += raw_output_actor
+  }
+
+  override def removeNotify()
+  {
+    Isabelle.session.raw_output -= raw_output_actor
+    super.removeNotify()
+  }
+}