simplified dockables using class Dockable;

--- a/src/Tools/jEdit/src/jedit/dockable.scala	Sat May 22 21:48:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/dockable.scala	Sat May 22 22:05:41 2010 +0200
@@ -21,7 +21,8 @@
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  def set_content(c: Component) = add(c, BorderLayout.CENTER)
+  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
+  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
 
   protected def init() { }
   protected def exit() { }

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat May 22 21:48:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat May 22 22:05:41 2010 +0200
@@ -14,20 +14,14 @@
 import scala.swing.{FlowPanel, Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
-import javax.swing.JPanel
-import java.awt.{BorderLayout, Dimension}
+import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
 
 
-class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+class Output_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-
   val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
   add(html_panel, BorderLayout.CENTER)
 
@@ -81,7 +75,7 @@
           val document = model.recent_document
           document.command_at(view.getTextArea.getCaretPosition) match {
             case Some((cmd, _)) =>
-              output_actor ! Render(filtered_results(document, cmd))
+              main_actor ! Render(filtered_results(document, cmd))
             case None =>
           }
         case None =>
@@ -97,9 +91,9 @@
     }
 
 
-  /* actor wiring */
+  /* main actor */
 
-  private val output_actor = actor {
+  private val main_actor = actor {
     loop {
       react {
         case Session.Global_Settings => handle_resize()
@@ -114,23 +108,21 @@
               html_panel.render(filtered_results(model.recent_document, cmd))
           }
 
-        case bad => System.err.println("output_actor: ignoring bad message " + bad)
+        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def addNotify()
+  override def init()
   {
-    super.addNotify()
-    Isabelle.session.results += output_actor
-    Isabelle.session.global_settings += output_actor
+    Isabelle.session.results += main_actor
+    Isabelle.session.global_settings += main_actor
   }
 
-  override def removeNotify()
+  override def exit()
   {
-    Isabelle.session.results -= output_actor
-    Isabelle.session.global_settings -= output_actor
-    super.removeNotify()
+    Isabelle.session.results -= main_actor
+    Isabelle.session.global_settings -= main_actor
   }
 
 

--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Sat May 22 21:48:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Sat May 22 22:05:41 2010 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/jedit/protocol_dockable.scala
     Author:     Makarius
 
-Dockable window for raw protocol messages.
+Dockable window for protocol messages.
 */
 
 package isabelle.jedit
@@ -10,45 +10,30 @@
 import isabelle._
 
 import scala.actors.Actor._
-
-import java.awt.{Dimension, Graphics, BorderLayout}
-import javax.swing.{JPanel, JTextArea, JScrollPane}
+import scala.swing.{TextArea, ScrollPane}
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
-class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-
-  private val text_area = new JTextArea
-  add(new JScrollPane(text_area), BorderLayout.CENTER)
+  private val text_area = new TextArea
+  set_content(new ScrollPane(text_area))
 
 
-  /* actor wiring */
+  /* main actor */
 
-  private val protocol_actor = actor {
+  private val main_actor = actor {
     loop {
       react {
         case result: Isabelle_Process.Result =>
           Swing_Thread.now { text_area.append(result.message.toString + "\n") }
 
-        case bad => System.err.println("protocol_actor: ignoring bad message " + bad)
+        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def addNotify()
-  {
-    super.addNotify()
-    Isabelle.session.raw_results += protocol_actor
-  }
-
-  override def removeNotify()
-  {
-    Isabelle.session.raw_results -= protocol_actor
-    super.removeNotify()
-  }
+  override def init() { Isabelle.session.raw_results += main_actor }
+  override def exit() { Isabelle.session.raw_results -= main_actor }
 }

--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat May 22 21:48:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat May 22 22:05:41 2010 +0200
@@ -10,45 +10,31 @@
 import isabelle._
 
 import scala.actors.Actor._
-
-import java.awt.{Dimension, Graphics, BorderLayout}
-import javax.swing.{JPanel, JTextArea, JScrollPane}
+import scala.swing.{TextArea, ScrollPane}
 
 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)
+class Raw_Output_Dockable(view: View, position: String)
+  extends Dockable(view: View, position: String)
 {
-  if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-
-  private val text_area = new JTextArea
-  add(new JScrollPane(text_area), BorderLayout.CENTER)
+  private val text_area = new TextArea
+  set_content(new ScrollPane(text_area))
 
 
-  /* actor wiring */
+  /* main actor */
 
-  private val raw_output_actor = actor {
+  private val main_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)
+        case bad => System.err.println("Raw_Output_Dockable: 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()
-  }
+  override def init() { Isabelle.session.raw_output += main_actor }
+  override def exit() { Isabelle.session.raw_output -= main_actor }
 }