src/Tools/jEdit/src/jedit/StateViewDockable.scala
author immler@in.tum.de
Thu Aug 27 10:51:09 2009 +0200 (2009-08-27)
changeset 34669 73727c7eec64
parent 34552 65f1b2261cc6
child 34745 83b553bd3fa3
permissions -rw-r--r--
state_update global in Plugin
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@34438
    14
import isabelle.renderer.UserAgent
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
wenzelm@34428
    50
        })
wenzelm@34428
    51
    }
wenzelm@34428
    52
  }
wenzelm@34428
    53
wenzelm@34434
    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@34669
    62
  // register for state-view
immler@34669
    63
  Isabelle.plugin.state_update += (cmd => {
immler@34669
    64
    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
immler@34669
    65
    if (cmd == null)
immler@34669
    66
      panel.setDocument(null: org.w3c.dom.Document)
immler@34669
    67
    else
immler@34669
    68
      panel.setDocument(cmd.result_document(theory_view.current_document()),
immler@34669
    69
        UserAgent.base_URL)
immler@34669
    70
  })
immler@34361
    71
immler@34406
    72
  private val fontResolver =
immler@34406
    73
    panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
wenzelm@34440
    74
  if (Isabelle.plugin.font != null)
wenzelm@34440
    75
    fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
immler@34406
    76
wenzelm@34456
    77
  Isabelle.plugin.font_changed += (font => {
wenzelm@34440
    78
    if (Isabelle.plugin.font != null)
wenzelm@34440
    79
      fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
wenzelm@34318
    80
immler@34406
    81
    panel.relayout()
immler@34406
    82
  })
immler@34406
    83
wenzelm@34318
    84
}