# HG changeset patch
# User wenzelm
# Date 1260310687 -3600
# Node ID 1a79c9b9af825fc42b7c042de7a8e55135c25e9c
# Parent  b63a88e2d75ab23160adcfbe48a665aab3e29361
proper actor wiring for raw process output;
unified Swing component setup;

diff -r b63a88e2d75a -r 1a79c9b9af82 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 23:15:59 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 23:18:07 2009 +0100
@@ -86,8 +86,9 @@
 {
   /* event buses */
 
+  val properties_changed = new Event_Bus[Unit]
+  val raw_results = new Event_Bus[Isabelle_Process.Result]
   val state_update = new Event_Bus[Command]
-  val properties_changed = new Event_Bus[Unit]
 
 
   /* selected state */
diff -r b63a88e2d75a -r 1a79c9b9af82 src/Tools/jEdit/src/jedit/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 23:15:59 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 23:18:07 2009 +0100
@@ -1,14 +1,15 @@
 /*
  * Dockable window for raw process output
  *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
+ * @author Makarius
  */
 
 package isabelle.jedit
 
 
-import java.awt.{Dimension, Graphics, GridLayout}
+import scala.actors.Actor._
+
+import java.awt.{Dimension, Graphics, BorderLayout}
 import javax.swing.{JPanel, JTextArea, JScrollPane}
 
 import org.gjt.sp.jedit.View
@@ -17,15 +18,42 @@
 
 class Raw_Output_Dockable(view: View, position: String) extends JPanel
 {
+  // outer panel
+
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  setLayout(new GridLayout(1, 1))
-  add(new JScrollPane(new JTextArea))
+  setLayout(new BorderLayout)
+
+
+  // text area
+
+  private val text_area = new JTextArea
+  add(new JScrollPane(text_area), BorderLayout.CENTER)
+
+
+  /* actor wiring */
 
-  def set_text(output_text_view: JTextArea) {
-    removeAll()
-    add(new JScrollPane(output_text_view))
-    revalidate()
+  private val raw_actor = actor {
+    loop {
+      react {
+        case result: Isabelle_Process.Result =>
+          Swing_Thread.now { text_area.append(result.toString + "\n") }
+
+        case bad => System.err.println("raw_actor: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def addNotify()
+  {
+    super.addNotify()
+    Isabelle.plugin.raw_results += raw_actor
+  }
+
+  override def removeNotify()
+  {
+    Isabelle.plugin.raw_results -= raw_actor
+    super.removeNotify()
   }
 }
diff -r b63a88e2d75a -r 1a79c9b9af82 src/Tools/jEdit/src/proofdocument/prover.scala
--- a/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 23:15:59 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 23:18:07 2009 +0100
@@ -77,13 +77,9 @@
 
   /* prover results */
 
-  val output_text_view = new JTextArea    // FIXME separate jEdit component
-
   private def handle_result(result: Isabelle_Process.Result)
   {
-    // FIXME separate jEdit component
-    Swing_Thread.later { output_text_view.append(result.toString + "\n") }
-
+    Isabelle.plugin.raw_results.event(result)
     val message = Isabelle_Process.parse_message(system, result)
 
     val state =
diff -r b63a88e2d75a -r 1a79c9b9af82 src/Tools/jEdit/src/proofdocument/theory_view.scala
--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 23:15:59 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 23:18:07 2009 +0100
@@ -174,19 +174,11 @@
       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
     buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
     buffer.addBufferListener(buffer_listener)
-
-    val dockable =
-      text_area.getView.getDockableWindowManager.getDockable("isabelle-raw-output")
-    if (dockable != null) {
-      val output_dockable = dockable.asInstanceOf[Raw_Output_Dockable]
-      val output_text_view = prover.output_text_view
-      output_dockable.set_text(output_text_view)
-    }
-
     buffer.propertiesChanged()
   }
 
-  def deactivate() {
+  def deactivate()
+  {
     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     buffer.removeBufferListener(buffer_listener)
     text_area.getPainter.removeExtension(text_area_extension)