src/Tools/jEdit/src/jedit/StateViewDockable.scala
author wenzelm
Sun Dec 21 19:51:56 2008 +0100 (2008-12-21)
changeset 34428 d69fd18f37f9
parent 34424 c880492754d0
child 34434 ba08fc74f98a
permissions -rw-r--r--
basic setup of anti-aliasing, according to jEdit property;
tuned;
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@34428
    16
import org.xhtmlrenderer.simple.{XHTMLPanel, FSScrollPane}
wenzelm@34318
    17
import org.xhtmlrenderer.context.AWTFontResolver
wenzelm@34428
    18
import org.xhtmlrenderer.layout.SharedContext;
wenzelm@34428
    19
import org.xhtmlrenderer.extend.TextRenderer;
wenzelm@34428
    20
import org.xhtmlrenderer.swing.Java2DTextRenderer;
wenzelm@34318
    21
wenzelm@34428
    22
import org.gjt.sp.jedit.jEdit
wenzelm@34318
    23
import org.gjt.sp.jedit.View
wenzelm@34424
    24
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@34428
    25
import org.gjt.sp.jedit.textarea.AntiAlias
wenzelm@34424
    26
wenzelm@34318
    27
wenzelm@34318
    28
class StateViewDockable(view : View, position : String) extends JPanel {
wenzelm@34424
    29
wenzelm@34428
    30
  // outer panel
wenzelm@34424
    31
  if (position == DockableWindowManager.FLOATING)
wenzelm@34424
    32
    setPreferredSize(new Dimension(500, 250))
immler@34406
    33
  setLayout(new BorderLayout)
immler@34406
    34
wenzelm@34428
    35
wenzelm@34428
    36
  // XHTML panel
wenzelm@34428
    37
  val panel = new XHTMLPanel(new UserAgent)
wenzelm@34428
    38
immler@34361
    39
wenzelm@34428
    40
  // anti-aliasing
wenzelm@34428
    41
  // TODO: proper EditBus event handling
wenzelm@34428
    42
  {
wenzelm@34428
    43
    val aa = jEdit.getProperty("view.antiAlias")
wenzelm@34428
    44
    if (aa != null && aa != AntiAlias.NONE) {
wenzelm@34428
    45
      panel.getSharedContext.setTextRenderer(
wenzelm@34428
    46
        {
wenzelm@34428
    47
          val renderer = new Java2DTextRenderer
wenzelm@34428
    48
          renderer.setSmoothingThreshold(0)
wenzelm@34428
    49
          renderer.setSmoothingLevel(TextRenderer.HIGH)
wenzelm@34428
    50
          renderer
wenzelm@34428
    51
        })
wenzelm@34428
    52
    }
wenzelm@34428
    53
  }
wenzelm@34428
    54
wenzelm@34428
    55
  // copy & paste
wenzelm@34428
    56
  (new SelectionActions).install(panel)
wenzelm@34428
    57
wenzelm@34428
    58
wenzelm@34428
    59
  // scrolling
wenzelm@34428
    60
  add(new FSScrollPane(panel), BorderLayout.CENTER)
wenzelm@34428
    61
immler@34361
    62
immler@34406
    63
  private val fontResolver =
immler@34406
    64
    panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
immler@34406
    65
  if (Plugin.plugin.viewFont != null)
immler@34406
    66
    fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
immler@34406
    67
immler@34406
    68
  Plugin.plugin.viewFontChanged.add(font => {
wenzelm@34318
    69
    if (Plugin.plugin.viewFont != null)
wenzelm@34318
    70
      fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
wenzelm@34318
    71
immler@34406
    72
    panel.relayout()
immler@34406
    73
  })
immler@34406
    74
wenzelm@34318
    75
}