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

     2.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat May 22 21:48:01 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat May 22 22:05:41 2010 +0200
     2.3 @@ -14,20 +14,14 @@
     2.4  import scala.swing.{FlowPanel, Button, CheckBox}
     2.5  import scala.swing.event.ButtonClicked
     2.6  
     2.7 -import javax.swing.JPanel
     2.8 -import java.awt.{BorderLayout, Dimension}
     2.9 +import java.awt.BorderLayout
    2.10  import java.awt.event.{ComponentEvent, ComponentAdapter}
    2.11  
    2.12  import org.gjt.sp.jedit.View
    2.13 -import org.gjt.sp.jedit.gui.DockableWindowManager
    2.14  
    2.15  
    2.16 -
    2.17 -class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
    2.18 +class Output_Dockable(view: View, position: String) extends Dockable(view, position)
    2.19  {
    2.20 -  if (position == DockableWindowManager.FLOATING)
    2.21 -    setPreferredSize(new Dimension(500, 250))
    2.22 -
    2.23    val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
    2.24    add(html_panel, BorderLayout.CENTER)
    2.25  
    2.26 @@ -81,7 +75,7 @@
    2.27            val document = model.recent_document
    2.28            document.command_at(view.getTextArea.getCaretPosition) match {
    2.29              case Some((cmd, _)) =>
    2.30 -              output_actor ! Render(filtered_results(document, cmd))
    2.31 +              main_actor ! Render(filtered_results(document, cmd))
    2.32              case None =>
    2.33            }
    2.34          case None =>
    2.35 @@ -97,9 +91,9 @@
    2.36      }
    2.37  
    2.38  
    2.39 -  /* actor wiring */
    2.40 +  /* main actor */
    2.41  
    2.42 -  private val output_actor = actor {
    2.43 +  private val main_actor = actor {
    2.44      loop {
    2.45        react {
    2.46          case Session.Global_Settings => handle_resize()
    2.47 @@ -114,23 +108,21 @@
    2.48                html_panel.render(filtered_results(model.recent_document, cmd))
    2.49            }
    2.50  
    2.51 -        case bad => System.err.println("output_actor: ignoring bad message " + bad)
    2.52 +        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    2.53        }
    2.54      }
    2.55    }
    2.56  
    2.57 -  override def addNotify()
    2.58 +  override def init()
    2.59    {
    2.60 -    super.addNotify()
    2.61 -    Isabelle.session.results += output_actor
    2.62 -    Isabelle.session.global_settings += output_actor
    2.63 +    Isabelle.session.results += main_actor
    2.64 +    Isabelle.session.global_settings += main_actor
    2.65    }
    2.66  
    2.67 -  override def removeNotify()
    2.68 +  override def exit()
    2.69    {
    2.70 -    Isabelle.session.results -= output_actor
    2.71 -    Isabelle.session.global_settings -= output_actor
    2.72 -    super.removeNotify()
    2.73 +    Isabelle.session.results -= main_actor
    2.74 +    Isabelle.session.global_settings -= main_actor
    2.75    }
    2.76  
    2.77  

     3.1 --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Sat May 22 21:48:01 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Sat May 22 22:05:41 2010 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  /*  Title:      Tools/jEdit/src/jedit/protocol_dockable.scala
     3.5      Author:     Makarius
     3.6  
     3.7 -Dockable window for raw protocol messages.
     3.8 +Dockable window for protocol messages.
     3.9  */
    3.10  
    3.11  package isabelle.jedit
    3.12 @@ -10,45 +10,30 @@
    3.13  import isabelle._
    3.14  
    3.15  import scala.actors.Actor._
    3.16 -
    3.17 -import java.awt.{Dimension, Graphics, BorderLayout}
    3.18 -import javax.swing.{JPanel, JTextArea, JScrollPane}
    3.19 +import scala.swing.{TextArea, ScrollPane}
    3.20  
    3.21  import org.gjt.sp.jedit.View
    3.22 -import org.gjt.sp.jedit.gui.DockableWindowManager
    3.23  
    3.24  
    3.25 -class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
    3.26 +class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
    3.27  {
    3.28 -  if (position == DockableWindowManager.FLOATING)
    3.29 -    setPreferredSize(new Dimension(500, 250))
    3.30 +  private val text_area = new TextArea
    3.31 +  set_content(new ScrollPane(text_area))
    3.32  
    3.33 -  private val text_area = new JTextArea
    3.34 -  add(new JScrollPane(text_area), BorderLayout.CENTER)
    3.35  
    3.36 +  /* main actor */
    3.37  
    3.38 -  /* actor wiring */
    3.39 -
    3.40 -  private val protocol_actor = actor {
    3.41 +  private val main_actor = actor {
    3.42      loop {
    3.43        react {
    3.44          case result: Isabelle_Process.Result =>
    3.45            Swing_Thread.now { text_area.append(result.message.toString + "\n") }
    3.46  
    3.47 -        case bad => System.err.println("protocol_actor: ignoring bad message " + bad)
    3.48 +        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    3.49        }
    3.50      }
    3.51    }
    3.52  
    3.53 -  override def addNotify()
    3.54 -  {
    3.55 -    super.addNotify()
    3.56 -    Isabelle.session.raw_results += protocol_actor
    3.57 -  }
    3.58 -
    3.59 -  override def removeNotify()
    3.60 -  {
    3.61 -    Isabelle.session.raw_results -= protocol_actor
    3.62 -    super.removeNotify()
    3.63 -  }
    3.64 +  override def init() { Isabelle.session.raw_results += main_actor }
    3.65 +  override def exit() { Isabelle.session.raw_results -= main_actor }
    3.66  }

     4.1 --- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat May 22 21:48:01 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Sat May 22 22:05:41 2010 +0200
     4.3 @@ -10,45 +10,31 @@
     4.4  import isabelle._
     4.5  
     4.6  import scala.actors.Actor._
     4.7 -
     4.8 -import java.awt.{Dimension, Graphics, BorderLayout}
     4.9 -import javax.swing.{JPanel, JTextArea, JScrollPane}
    4.10 +import scala.swing.{TextArea, ScrollPane}
    4.11  
    4.12  import org.gjt.sp.jedit.View
    4.13 -import org.gjt.sp.jedit.gui.DockableWindowManager
    4.14  
    4.15  
    4.16 -class Raw_Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
    4.17 +class Raw_Output_Dockable(view: View, position: String)
    4.18 +  extends Dockable(view: View, position: String)
    4.19  {
    4.20 -  if (position == DockableWindowManager.FLOATING)
    4.21 -    setPreferredSize(new Dimension(500, 250))
    4.22 +  private val text_area = new TextArea
    4.23 +  set_content(new ScrollPane(text_area))
    4.24  
    4.25 -  private val text_area = new JTextArea
    4.26 -  add(new JScrollPane(text_area), BorderLayout.CENTER)
    4.27  
    4.28 +  /* main actor */
    4.29  
    4.30 -  /* actor wiring */
    4.31 -
    4.32 -  private val raw_output_actor = actor {
    4.33 +  private val main_actor = actor {
    4.34      loop {
    4.35        react {
    4.36          case result: Isabelle_Process.Result =>
    4.37            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
    4.38  
    4.39 -        case bad => System.err.println("raw_output_actor: ignoring bad message " + bad)
    4.40 +        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
    4.41        }
    4.42      }
    4.43    }
    4.44  
    4.45 -  override def addNotify()
    4.46 -  {
    4.47 -    super.addNotify()
    4.48 -    Isabelle.session.raw_output += raw_output_actor
    4.49 -  }
    4.50 -
    4.51 -  override def removeNotify()
    4.52 -  {
    4.53 -    Isabelle.session.raw_output -= raw_output_actor
    4.54 -    super.removeNotify()
    4.55 -  }
    4.56 +  override def init() { Isabelle.session.raw_output += main_actor }
    4.57 +  override def exit() { Isabelle.session.raw_output -= main_actor }
    4.58  }