renamed Plugin.plugin to Plugin.self;
authorwenzelm
Sun, 21 Dec 2008 21:43:41 +0100
changeset 34435 926272164bff
parent 34434 ba08fc74f98a
child 34436 a77cfbe18a31
renamed Plugin.plugin to Plugin.self; use Plugin.self.symbols; tuned;
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) {
+  }
 }