src/Tools/jEdit/src/jedit/results_dockable.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34765 63ba7f0931e2
     1.1 --- a/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -7,13 +7,14 @@
     1.4  
     1.5  package isabelle.jedit
     1.6  
     1.7 +
     1.8  import isabelle.XML
     1.9  
    1.10 +import scala.swing.{BorderPanel, Component}
    1.11 +
    1.12  import java.io.StringReader
    1.13  import java.awt.{BorderLayout, Dimension}
    1.14 -
    1.15  import javax.swing.{JButton, JPanel, JScrollPane}
    1.16 -
    1.17  import java.util.logging.{Logger, Level}
    1.18  
    1.19  import org.lobobrowser.html.parser._
    1.20 @@ -31,12 +32,12 @@
    1.21  import scala.io.Source
    1.22  
    1.23  
    1.24 -class StateViewDockable(view : View, position : String) extends JPanel {
    1.25 -
    1.26 +class Results_Dockable(view : View, position : String) extends BorderPanel
    1.27 +{
    1.28    // outer panel
    1.29 +
    1.30    if (position == DockableWindowManager.FLOATING)
    1.31 -    setPreferredSize(new Dimension(500, 250))
    1.32 -  setLayout(new BorderLayout)
    1.33 +    preferredSize = new Dimension(500, 250)
    1.34  
    1.35  
    1.36    // global logging
    1.37 @@ -87,7 +88,8 @@
    1.38    doc.appendChild(empty_body)
    1.39  
    1.40    panel.setDocument(doc, rcontext)
    1.41 -  add(panel, BorderLayout.CENTER)
    1.42 +
    1.43 +  add(Component.wrap(panel), BorderPanel.Position.Center)
    1.44  
    1.45    
    1.46    // register for state-view