# HG changeset patch
# User immler@in.tum.de
# Date 1227041902 -3600
# Node ID 2b730e933006504e02568eb4095885bef0477e2e
# Parent  d6d536e5d7e6da49a2b461607bfcd4c17d24fd23
convert eg pasted xsymbols

diff -r d6d536e5d7e6 -r 2b730e933006 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Nov 18 21:47:33 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Nov 18 21:58:22 2008 +0100
@@ -204,7 +204,7 @@
   override def preContentInserted(buffer : JEditBuffer, startLine : Int,
 			offset : Int, numLines : Int, length : Int) {
     //simple xsymbol detection: entering whitespace after '>' checks for xsymbol
-    if(offset - 1 > 0 && buffer.getText(offset - 1, 2).equals("> ")){
+    if(length == 1 && offset - 1 > 0 && buffer.getText(offset - 1, 2).equals("> ")){
       val MAX_XSYMB_LENGTH = 20
       var beginning = offset - 2
       var length = 2
@@ -218,7 +218,16 @@
         buffer.remove(beginning, length)
         buffer.insert(beginning, decoded)
       }
+    } else {
+      //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)
+      }
     }
+
     if (col == null)
       col = new Changed(offset, length, 0)
     else if (col.start <= offset && offset <= col.start + col.added)