--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Nov 10 17:32:07 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Nov 10 19:31:27 2008 +0100
@@ -56,7 +56,6 @@
//Render a message to a Panel
def render (message: Document): XHTMLPanel = {
val panel = new XHTMLPanel(new UserAgent())
- panel.setFontScalingFactor(.5f)
val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
if (Plugin.plugin.viewFont != null)
@@ -78,7 +77,7 @@
def calculate_preferred_size(panel: XHTMLPanel){
message_view.add (panel)
panel.setBounds (0, 0, message_view.getWidth, 1) // document has to fit into width
- panel.doLayout (panel.getGraphics) //lay out, preferred size is set then
+ panel.doDocumentLayout (panel.getGraphics) //lay out, preferred size is set then
// if there are thousands of empty panels, all have to be rendered -
// but this takes time (even for empty panels); therefore minimum size
panel.setPreferredSize(new java.awt.Dimension(message_view.getWidth,Math.max(50, panel.getPreferredSize.getHeight.toInt)))
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Nov 10 17:32:07 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Nov 10 19:31:27 2008 +0100
@@ -1,8 +1,8 @@
package isabelle.jedit
-import java.awt.GridLayout
-import javax.swing.{ JPanel, JScrollPane }
+import java.awt.BorderLayout
+import javax.swing.{ JButton, JPanel, JScrollPane }
import isabelle.IsabelleSystem.getenv
@@ -13,11 +13,29 @@
import org.gjt.sp.jedit.View
+//Copy-Paste-support
+import org.w3c.dom.ranges.Range
+import org.w3c.dom.DocumentFragment
+import org.xhtmlrenderer.swing.SelectionHighlighter
+
class StateViewDockable(view : View, position : String) extends JPanel {
{
val panel = new XHTMLPanel(new UserAgent())
- setLayout(new GridLayout(1, 1))
- add(new JScrollPane(panel))
+ setLayout(new BorderLayout)
+
+ //Copy-paste-support
+ val sel_highlighter = new SelectionHighlighter
+
+ val copyaction = new SelectionHighlighter.CopyAction {
+ override def actionPerformed(e: java.awt.event.ActionEvent) {
+ System.err.println (sel_highlighter.getSelectionRange)
+ }
+ }
+ copyaction.install(sel_highlighter)
+ sel_highlighter.install(panel)
+ add(new JButton(copyaction), BorderLayout.SOUTH)
+
+ add(new JScrollPane(panel), BorderLayout.CENTER)
val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]