selecting text of state view
authorimmler@in.tum.de
Mon, 10 Nov 2008 19:31:27 +0100
changeset 343643e7568e833d9
parent 34363 b7af69a030a1
child 34365 917af128270b
selecting text of state view
src/Tools/jEdit/src/jedit/ScrollerDockable.scala
src/Tools/jEdit/src/jedit/StateViewDockable.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 10 17:32:07 2008 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 10 19:31:27 2008 +0100
     1.3 @@ -56,7 +56,6 @@
     1.4    //Render a message to a Panel
     1.5    def render (message: Document): XHTMLPanel = {
     1.6      val panel = new XHTMLPanel(new UserAgent())
     1.7 -    panel.setFontScalingFactor(.5f)
     1.8      val fontResolver =
     1.9        panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
    1.10      if (Plugin.plugin.viewFont != null)
    1.11 @@ -78,7 +77,7 @@
    1.12    def calculate_preferred_size(panel: XHTMLPanel){
    1.13      message_view.add (panel)
    1.14      panel.setBounds (0, 0, message_view.getWidth, 1) // document has to fit into width
    1.15 -    panel.doLayout (panel.getGraphics) //lay out, preferred size is set then
    1.16 +    panel.doDocumentLayout (panel.getGraphics) //lay out, preferred size is set then
    1.17      // if there are thousands of empty panels, all have to be rendered -
    1.18      // but this takes time (even for empty panels); therefore minimum size
    1.19      panel.setPreferredSize(new java.awt.Dimension(message_view.getWidth,Math.max(50, panel.getPreferredSize.getHeight.toInt)))
     2.1 --- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Nov 10 17:32:07 2008 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Nov 10 19:31:27 2008 +0100
     2.3 @@ -1,8 +1,8 @@
     2.4  package isabelle.jedit
     2.5  
     2.6  
     2.7 -import java.awt.GridLayout
     2.8 -import javax.swing.{ JPanel, JScrollPane }
     2.9 +import java.awt.BorderLayout
    2.10 +import javax.swing.{ JButton, JPanel, JScrollPane }
    2.11  
    2.12  import isabelle.IsabelleSystem.getenv
    2.13  
    2.14 @@ -13,11 +13,29 @@
    2.15  
    2.16  import org.gjt.sp.jedit.View
    2.17  
    2.18 +//Copy-Paste-support
    2.19 +import org.w3c.dom.ranges.Range
    2.20 +import org.w3c.dom.DocumentFragment
    2.21 +import org.xhtmlrenderer.swing.SelectionHighlighter
    2.22 +
    2.23  class StateViewDockable(view : View, position : String) extends JPanel {
    2.24    {
    2.25      val panel = new XHTMLPanel(new UserAgent())
    2.26 -    setLayout(new GridLayout(1, 1))
    2.27 -    add(new JScrollPane(panel))
    2.28 +    setLayout(new BorderLayout)
    2.29 +
    2.30 +    //Copy-paste-support
    2.31 +    val sel_highlighter = new SelectionHighlighter
    2.32 +
    2.33 +    val copyaction = new SelectionHighlighter.CopyAction {
    2.34 +      override def actionPerformed(e: java.awt.event.ActionEvent) {
    2.35 +        System.err.println (sel_highlighter.getSelectionRange)
    2.36 +      }
    2.37 +    }
    2.38 +    copyaction.install(sel_highlighter)
    2.39 +    sel_highlighter.install(panel)
    2.40 +    add(new JButton(copyaction), BorderLayout.SOUTH)
    2.41 +
    2.42 +    add(new JScrollPane(panel), BorderLayout.CENTER)
    2.43      
    2.44      val fontResolver =
    2.45        panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]