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]