src/Tools/jEdit/src/jedit/StateViewDockable.scala
author wenzelm
Sun, 21 Dec 2008 22:09:33 +0100
changeset 34438 2faedc70b52d
parent 34434 ba08fc74f98a
child 34440 561a6d19bd95
permissions -rw-r--r--
proper import isabelle.renderer.UserAgent;

/*
 * Dockable window with rendered state output
 *
 * @author Fabian Immler, TU Munich
 * @author Johannes Hölzl, TU Munich
 */

package isabelle.jedit


import java.awt.{BorderLayout, Dimension}
import javax.swing.{JButton, JPanel, JScrollPane}

import isabelle.IsabelleSystem.getenv
import isabelle.renderer.UserAgent

import org.xhtmlrenderer.simple.{XHTMLPanel, FSScrollPane}
import org.xhtmlrenderer.context.AWTFontResolver
import org.xhtmlrenderer.layout.SharedContext;
import org.xhtmlrenderer.extend.TextRenderer;
import org.xhtmlrenderer.swing.Java2DTextRenderer;

import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.DockableWindowManager
import org.gjt.sp.jedit.textarea.AntiAlias


class StateViewDockable(view : View, position : String) extends JPanel {

  // outer panel
  if (position == DockableWindowManager.FLOATING)
    setPreferredSize(new Dimension(500, 250))
  setLayout(new BorderLayout)


  // XHTML panel
  val panel = new XHTMLPanel(new UserAgent)


  // anti-aliasing
  // TODO: proper EditBus event handling
  {
    val aa = jEdit.getProperty("view.antiAlias")
    if (aa != null && aa != AntiAlias.NONE) {
      panel.getSharedContext.setTextRenderer(
        {
          val renderer = new Java2DTextRenderer
          renderer.setSmoothingThreshold(0)
          renderer.setSmoothingLevel(TextRenderer.HIGH)
          renderer
        })
    }
  }

  
  // copy & paste
  (new SelectionActions).install(panel)


  // scrolling
  add(new FSScrollPane(panel), BorderLayout.CENTER)


  private val fontResolver =
    panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
  if (Plugin.self.font != null)
    fontResolver.setFontMapping("Isabelle", Plugin.self.font)

  Plugin.self.font_changed.add(font => {
    if (Plugin.self.font != null)
      fontResolver.setFontMapping("Isabelle", Plugin.self.font)

    panel.relayout()
  })

}