# HG changeset patch
# User immler@in.tum.de
# Date 1226341887 -3600
# Node ID 3e7568e833d975eef866acb9bd52b586ee70a726
# Parent  b7af69a030a1e95871eac4f389ff9004101a043f
selecting text of state view

diff -r b7af69a030a1 -r 3e7568e833d9 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- 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)))
diff -r b7af69a030a1 -r 3e7568e833d9 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- 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]