src/Tools/jEdit/src/jedit/StateViewDockable.scala
author wenzelm
Sat Dec 20 17:41:57 2008 +0100 (2008-12-20)
changeset 34424 c880492754d0
parent 34408 ad7b6c4813c8
child 34428 d69fd18f37f9
permissions -rw-r--r--
setPreferredSize for floating dockables;
wenzelm@34408
     1
/*
wenzelm@34408
     2
 * Dockable window with rendered state output
wenzelm@34408
     3
 *
wenzelm@34408
     4
 * @author Fabian Immler, TU Munich
wenzelm@34408
     5
 * @author Johannes Hölzl, TU Munich
wenzelm@34408
     6
 */
wenzelm@34408
     7
wenzelm@34318
     8
package isabelle.jedit
wenzelm@34318
     9
wenzelm@34318
    10
wenzelm@34424
    11
import java.awt.{BorderLayout, Dimension}
wenzelm@34424
    12
import javax.swing.{JButton, JPanel, JScrollPane}
wenzelm@34318
    13
wenzelm@34318
    14
import isabelle.IsabelleSystem.getenv
wenzelm@34318
    15
wenzelm@34318
    16
import org.xhtmlrenderer.simple.XHTMLPanel
wenzelm@34318
    17
import org.xhtmlrenderer.context.AWTFontResolver
wenzelm@34318
    18
wenzelm@34318
    19
import org.gjt.sp.jedit.View
wenzelm@34424
    20
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@34424
    21
wenzelm@34318
    22
wenzelm@34318
    23
class StateViewDockable(view : View, position : String) extends JPanel {
immler@34406
    24
  val panel = new XHTMLPanel(new UserAgent())
wenzelm@34424
    25
wenzelm@34424
    26
  if (position == DockableWindowManager.FLOATING)
wenzelm@34424
    27
    setPreferredSize(new Dimension(500, 250))
wenzelm@34424
    28
immler@34406
    29
  setLayout(new BorderLayout)
immler@34406
    30
wenzelm@34424
    31
  
immler@34406
    32
  //Copy-paste-support
immler@34406
    33
  private val cp = new SelectionActions
immler@34406
    34
  cp.install(panel)
immler@34361
    35
immler@34406
    36
  add(new JScrollPane(panel), BorderLayout.CENTER)
immler@34361
    37
immler@34406
    38
  private val fontResolver =
immler@34406
    39
    panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
immler@34406
    40
  if (Plugin.plugin.viewFont != null)
immler@34406
    41
    fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
immler@34406
    42
immler@34406
    43
  Plugin.plugin.viewFontChanged.add(font => {
wenzelm@34318
    44
    if (Plugin.plugin.viewFont != null)
wenzelm@34318
    45
      fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
wenzelm@34318
    46
immler@34406
    47
    panel.relayout()
immler@34406
    48
  })
immler@34406
    49
wenzelm@34318
    50
}