# HG changeset patch
# User wenzelm
# Date 1229892221 -3600
# Node ID 926272164bffc053bf3ee5976de4cd12e46eb48c
# Parent  ba08fc74f98abf7c2d545976a857f49c0904ce6b
renamed Plugin.plugin to Plugin.self;
use Plugin.self.symbols;
tuned;

diff -r ba08fc74f98a -r 926272164bff src/Tools/jEdit/src/jedit/SelectionActions.scala
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala	Sun Dec 21 21:43:41 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala	Sun Dec 21 21:43:41 2008 +0100
@@ -25,24 +25,22 @@
 
   def copyaction {
       val selected_string = getSelectionRange.toString
-      val encoded = VFS.converter.encode (selected_string)
+      val encoded = Plugin.self.symbols.encode(selected_string)
       val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
       val transferable = new java.awt.datatransfer.StringSelection(selected_string)
       clipboard.setContents(transferable, null)
   }
   
-  override def keyPressed (e: KeyEvent) {
+  override def keyPressed(e: KeyEvent) {
     if(e.getKeyCode == KeyEvent.VK_ENTER) {
       copyaction
       e.consume
     }
   }
-  override def keyReleased (e: KeyEvent) {
-    
-  }
-  override def keyTyped (e: KeyEvent) {
-    
+  
+  override def keyReleased(e: KeyEvent) {
   }
 
-
+  override def keyTyped(e: KeyEvent) {
+  }
 }