# HG changeset patch
# User immler@in.tum.de
# Date 1227042906 -3600
# Node ID 71e86ec7e159c2d671de5c2b9a9d76e9b2b87ac9
# Parent  b41c1b50e0a988e49fcb35d2c46046806d58553c
replacing xsymbols *after* inserting text

diff -r b41c1b50e0a9 -r 71e86ec7e159 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 22:07:40 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 22:15:06 2008 +0100
@@ -195,9 +195,9 @@
 
 
 //containing the unrendered messages
-class MessageBuffer extends ArrayBuffer[Document] with Unrendered[Document]{
+class MessageBuffer extends HashMap[Int,Document] with Unrendered[Document]{
   override def addUnrendered (id: Int, m: Document) {
-    append(m)
+    update(id, m)
   }
   override def getUnrendered (id: Int): Option[Document] = {
     if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
diff -r b41c1b50e0a9 -r 71e86ec7e159 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Nov 18 22:07:40 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Nov 18 22:15:06 2008 +0100
@@ -197,7 +197,18 @@
   }
 	
   override def contentInserted(buffer : JEditBuffer, startLine : Int, 
-                               offset : Int, numLines : Int, length : 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)
+      }
+    }
+  }
   override def contentRemoved(buffer : JEditBuffer, startLine : Int, 
                               offset : Int, numLines : Int, length : Int) { }
 
@@ -218,14 +229,6 @@
         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)