# HG changeset patch
# User immler@in.tum.de
# Date 1227041129 -3600
# Node ID 4a63526bead10cb87873c456ad8082b713a6e155
# Parent  e0679b361a0e60ddbc9e302ee16a275a515f3090
copy-paste for XHTMLPanels

diff -r e0679b361a0e -r 4a63526bead1 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 15:41:01 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 21:45:29 2008 +0100
@@ -31,6 +31,7 @@
 }
 
 object Renderer {
+  
   def render (message: Document): XHTMLPanel = {
     val panel = new XHTMLPanel(new UserAgent())
     val fontResolver =
@@ -44,6 +45,8 @@
       panel.relayout()
     })
     panel.setDocument(message, UserAgent.baseURL)
+    val sa = new SelectionActions
+    sa.install(panel)
     panel
   }
   
diff -r e0679b361a0e -r 4a63526bead1 src/Tools/jEdit/src/jedit/SelectionActions.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala	Tue Nov 18 21:45:29 2008 +0100
@@ -0,0 +1,52 @@
+/*
+ * SelectionActions.scala
+ *
+ * To change this template, choose Tools | Template Manager
+ * and open the template in the editor.
+ */
+
+package isabelle.jedit
+
+import org.w3c.dom.ranges.Range
+import org.w3c.dom.DocumentFragment
+import org.xhtmlrenderer.swing.SelectionHighlighter
+import org.xhtmlrenderer.simple.XHTMLPanel
+
+import java.awt.event.{KeyListener, KeyEvent}
+
+import org.gjt.sp.jedit.gui._
+
+class SelectionActions extends SelectionHighlighter with KeyListener{
+
+  override def install(panel: XHTMLPanel) {
+    super.install(panel)
+    panel.addKeyListener(this)
+  }
+  
+
+  def copyaction {
+      val selected_string = getSelectionRange.toString
+      val encoded = VFS.converter.encode (selected_string)
+      mousePressed(new java.awt.event.MouseEvent(getComponent,0,0,0,0,0,0, false))
+      mouseReleased(new java.awt.event.MouseEvent(getComponent,0,0,0,0,0,0, false))
+      val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
+      val transferable = new java.awt.datatransfer.StringSelection(encoded)
+      clipboard.setContents(transferable, null)
+      super.install(getComponent)
+  }
+  
+  override def keyPressed (e: KeyEvent) {
+    if(e.getKeyCode == KeyEvent.VK_ENTER) {
+      copyaction
+      e.consume
+    }
+  }
+  override def keyReleased (e: KeyEvent) {
+    
+  }
+  override def keyTyped (e: KeyEvent) {
+    
+  }
+
+
+}
diff -r e0679b361a0e -r 4a63526bead1 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Tue Nov 18 15:41:01 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Tue Nov 18 21:45:29 2008 +0100
@@ -13,34 +13,14 @@
 
 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 BorderLayout)
 
     //Copy-paste-support
-    val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
-    val sel_highlighter = new SelectionHighlighter
-
-    val copyaction = new SelectionHighlighter.CopyAction {
-      override def actionPerformed(e: java.awt.event.ActionEvent) {
-        val selected_string = sel_highlighter.getSelectionRange.toString
-        val encoded = VFS.converter.encode (selected_string)
-        System.err.println ("-- copy --")
-        System.err.println (selected_string)
-        System.err.println (encoded)
-        val transferable = new java.awt.datatransfer.StringSelection(encoded)
-        clipboard.setContents(transferable, null)
-      }
-    }
-    copyaction.install(sel_highlighter)
-    sel_highlighter.install(panel)
-    add(new JButton(copyaction), BorderLayout.SOUTH)
+    val cp = new SelectionActions
+    cp.install(panel)
 
     add(new JScrollPane(panel), BorderLayout.CENTER)