# HG changeset patch
# User wenzelm
# Date 1260305370 -3600
# Node ID d8d321af147845d6b4e4af4b84900baa4170224e
# Parent  8dd19c5f8c56ffae2df02c4f4254696783bfe639
back to low-level JPanel, required for addNotify/removeNotify;
proper actor wiring, support multiple (floating) instances;

diff -r 8dd19c5f8c56 -r d8d321af1478 src/Tools/jEdit/plugin/dockables.xml
--- a/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 21:48:12 2009 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 21:49:30 2009 +0100
@@ -3,12 +3,12 @@
 
 <DOCKABLES>
 	<DOCKABLE NAME="isabelle-results" MOVABLE="TRUE">
-		new isabelle.jedit.Results_Dockable(view, position).peer();
+		new isabelle.jedit.Results_Dockable(view, position);
 	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
 		new isabelle.jedit.Raw_Output_Dockable(view, position);
 	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
-		new isabelle.jedit.History_Dockable(view, position).peer();
+		new isabelle.jedit.History_Dockable(view, position).peer ();
 	</DOCKABLE>
 </DOCKABLES>
\ No newline at end of file
diff -r 8dd19c5f8c56 -r d8d321af1478 src/Tools/jEdit/src/jedit/results_dockable.scala
--- a/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 21:48:12 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 21:49:30 2009 +0100
@@ -7,36 +7,69 @@
 package isabelle.jedit
 
 
-import isabelle.proofdocument.HTML_Panel
+import isabelle.proofdocument.{Command, HTML_Panel}
 
 import scala.io.Source
-import scala.swing.{BorderPanel, Component}
+import scala.actors.Actor._
 
-import java.awt.Dimension
+import javax.swing.JPanel
+import java.awt.{BorderLayout, Dimension}
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
 
-class Results_Dockable(view: View, position: String) extends BorderPanel
+class Results_Dockable(view: View, position: String) extends JPanel
 {
   // outer panel
 
   if (position == DockableWindowManager.FLOATING)
-    preferredSize = new Dimension(500, 250)
+    setPreferredSize(new Dimension(500, 250))
+  setLayout(new BorderLayout)
 
 
   // HTML panel
 
-  val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
-  add(Component.wrap(html_panel), BorderPanel.Position.Center)
+  private val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
+  add(html_panel, BorderLayout.CENTER)
+
+
+  /* actor wiring */
+
+  private val results_actor = actor {
+    loop {
+      react {
+        case cmd: Command =>
+          val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
+          val body =
+            if (cmd == null) Nil  // FIXME ??
+            else cmd.results(theory_view.current_document)
+          html_panel.render(body)
+          
+        case bad => System.err.println("prover: ignoring bad message " + bad)
+      }
+    }
+  }
 
-  Isabelle.plugin.state_update += (cmd => {
-    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
-    val body =
-      if (cmd == null) Nil  // FIXME ??
-      else cmd.results(theory_view.current_document)
-    html_panel.render(body)
-  })
+  private val properties_actor = actor {
+    loop {
+      react {
+        case _: Unit => html_panel.init(Isabelle.Int_Property("font-size"))
+        case bad => System.err.println("prover: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def addNotify() {
+    super.addNotify()
+    Isabelle.plugin.state_update += results_actor
+    Isabelle.plugin.properties_changed += properties_actor
+  }
+
+  override def removeNotify() {
+    Isabelle.plugin.state_update -= results_actor
+    Isabelle.plugin.properties_changed -= properties_actor
+    super.removeNotify()
+  }
 }