# HG changeset patch
# User immler@in.tum.de
# Date 1227821093 -3600
# Node ID d67fe0cb1106adae48729a992db31021024ae4a8
# Parent  b295fe78294ade60eb20006a3358533a1c2b5a15
removed xsymbol converting -> sidekick should do that

diff -r b295fe78294a -r d67fe0cb1106 src/Tools/jEdit/src/jedit/SelectionActions.scala
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala	Thu Nov 27 21:15:31 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala	Thu Nov 27 22:24:53 2008 +0100
@@ -27,12 +27,9 @@
   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)
+      val transferable = new java.awt.datatransfer.StringSelection(selected_string)
       clipboard.setContents(transferable, null)
-      super.install(getComponent)
   }
   
   override def keyPressed (e: KeyEvent) {
diff -r b295fe78294a -r d67fe0cb1106 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Nov 27 21:15:31 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Nov 27 22:24:53 2008 +0100
@@ -197,40 +197,12 @@
   }
 	
   override def contentInserted(buffer : JEditBuffer, startLine : Int, 
-                               offset : Int, numLines : Int, length : Int) {
-    
-     if(length > 1) {
-      //longer text inserted -> convert it
-      val text = buffer.getText(offset, length)
-      val decoded = VFS.converter.decode(text)
-      if(!text.equals(decoded)){
-        buffer.remove(offset, length)
-        buffer.insert(offset, decoded)
-      }
-    }
-  }
+                               offset : Int, numLines : Int, length : Int) { }
   override def contentRemoved(buffer : JEditBuffer, startLine : Int, 
                               offset : Int, numLines : Int, length : Int) { }
 
   override def preContentInserted(buffer : JEditBuffer, startLine : Int,
 			offset : Int, numLines : Int, length : Int) {
-    //simple xsymbol detection: entering whitespace after '>' checks for xsymbol
-    if(length == 1 && offset - 1 > 0 && buffer.getText(offset - 1, 2).equals("> ")){
-      val MAX_XSYMB_LENGTH = 20
-      var beginning = offset - 2
-      var length = 2
-      while(length < MAX_XSYMB_LENGTH && beginning > 0 && !buffer.getText(beginning, 1).equals("\\")){
-        beginning -= 1
-        length += 1
-      }
-      if(beginning >= 0 && buffer.getText(beginning, 2).equals("\\<")){
-        val candidate = buffer.getText(beginning, length)
-        val decoded = VFS.converter.decode(candidate)
-        buffer.remove(beginning, length)
-        buffer.insert(beginning, decoded)
-      }
-    }
-
     if (col == null)
       col = new Changed(offset, length, 0)
     else if (col.start <= offset && offset <= col.start + col.added)