# HG changeset patch
# User immler@in.tum.de
# Date 1226413668 -3600
# Node ID 917af128270b39555a26d2162801fcc84ba75718
# Parent  3e7568e833d975eef866acb9bd52b586ee70a726
copying selection to clipboard

diff -r 3e7568e833d9 -r 917af128270b src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Nov 10 19:31:27 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Tue Nov 11 15:27:48 2008 +0100
@@ -24,11 +24,19 @@
     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) {
-        System.err.println (sel_highlighter.getSelectionRange)
+        val inter = new isabelle.Symbol.Interpretation
+        val selected_string = sel_highlighter.getSelectionRange.toString
+        val encoded = inter.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)