1.1 --- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Nov 10 19:31:27 2008 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Tue Nov 11 15:27:48 2008 +0100
     1.3 @@ -24,11 +24,19 @@
     1.4      setLayout(new BorderLayout)
     1.5  
     1.6      //Copy-paste-support
     1.7 +    val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
     1.8      val sel_highlighter = new SelectionHighlighter
     1.9  
    1.10      val copyaction = new SelectionHighlighter.CopyAction {
    1.11        override def actionPerformed(e: java.awt.event.ActionEvent) {
    1.12 -        System.err.println (sel_highlighter.getSelectionRange)
    1.13 +        val inter = new isabelle.Symbol.Interpretation
    1.14 +        val selected_string = sel_highlighter.getSelectionRange.toString
    1.15 +        val encoded = inter.encode (selected_string)
    1.16 +        System.err.println ("-- copy --")
    1.17 +        System.err.println (selected_string)
    1.18 +        System.err.println (encoded)
    1.19 +        val transferable = new java.awt.datatransfer.StringSelection(encoded)
    1.20 +        clipboard.setContents(transferable, null)
    1.21        }
    1.22      }
    1.23      copyaction.install(sel_highlighter)