src/Tools/jEdit/src/jedit/StateViewDockable.scala
author immler@in.tum.de
Mon Nov 10 19:31:27 2008 +0100 (2008-11-10)
changeset 34361 3e7568e833d9
parent 34353 aa0d2f0bde83
child 34362 917af128270b
permissions -rw-r--r--
selecting text of state view
wenzelm@34318
     1
package isabelle.jedit
wenzelm@34318
     2
wenzelm@34318
     3
immler@34361
     4
import java.awt.BorderLayout
immler@34361
     5
import javax.swing.{ JButton, JPanel, JScrollPane }
wenzelm@34318
     6
wenzelm@34318
     7
import isabelle.IsabelleSystem.getenv
wenzelm@34318
     8
wenzelm@34318
     9
import org.w3c.dom.Document
wenzelm@34318
    10
wenzelm@34318
    11
import org.xhtmlrenderer.simple.XHTMLPanel
wenzelm@34318
    12
import org.xhtmlrenderer.context.AWTFontResolver
wenzelm@34318
    13
wenzelm@34318
    14
import org.gjt.sp.jedit.View
wenzelm@34318
    15
immler@34361
    16
//Copy-Paste-support
immler@34361
    17
import org.w3c.dom.ranges.Range
immler@34361
    18
import org.w3c.dom.DocumentFragment
immler@34361
    19
import org.xhtmlrenderer.swing.SelectionHighlighter
immler@34361
    20
wenzelm@34318
    21
class StateViewDockable(view : View, position : String) extends JPanel {
wenzelm@34318
    22
  {
wenzelm@34318
    23
    val panel = new XHTMLPanel(new UserAgent())
immler@34361
    24
    setLayout(new BorderLayout)
immler@34361
    25
immler@34361
    26
    //Copy-paste-support
immler@34361
    27
    val sel_highlighter = new SelectionHighlighter
immler@34361
    28
immler@34361
    29
    val copyaction = new SelectionHighlighter.CopyAction {
immler@34361
    30
      override def actionPerformed(e: java.awt.event.ActionEvent) {
immler@34361
    31
        System.err.println (sel_highlighter.getSelectionRange)
immler@34361
    32
      }
immler@34361
    33
    }
immler@34361
    34
    copyaction.install(sel_highlighter)
immler@34361
    35
    sel_highlighter.install(panel)
immler@34361
    36
    add(new JButton(copyaction), BorderLayout.SOUTH)
immler@34361
    37
immler@34361
    38
    add(new JScrollPane(panel), BorderLayout.CENTER)
wenzelm@34318
    39
    
wenzelm@34318
    40
    val fontResolver =
wenzelm@34318
    41
      panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
wenzelm@34318
    42
    if (Plugin.plugin.viewFont != null)
wenzelm@34318
    43
      fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
wenzelm@34318
    44
wenzelm@34318
    45
    Plugin.plugin.viewFontChanged.add(font => {
wenzelm@34318
    46
      if (Plugin.plugin.viewFont != null)
wenzelm@34318
    47
        fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
wenzelm@34318
    48
      
wenzelm@34318
    49
      panel.relayout()
wenzelm@34318
    50
    })
wenzelm@34318
    51
    
wenzelm@34318
    52
    Plugin.plugin.stateUpdate.add(state => {
wenzelm@34318
    53
      if (state == null)
wenzelm@34318
    54
        panel.setDocument(null : Document)
wenzelm@34318
    55
      else
immler@34353
    56
        panel.setDocument(state.document, UserAgent.baseURL)
wenzelm@34318
    57
    })
wenzelm@34318
    58
  }
wenzelm@34318
    59
}