# HG changeset patch
# User immler@in.tum.de
# Date 1227042460 -3600
# Node ID b41c1b50e0a988e49fcb35d2c46046806d58553c
# Parent  2b730e933006504e02568eb4095885bef0477e2e
buffer as array

diff -r 2b730e933006 -r b41c1b50e0a9 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 21:58:22 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 22:07:40 2008 +0100
@@ -195,9 +195,9 @@
 
 
 //containing the unrendered messages
-class MessageBuffer extends HashMap[Int,Document] with Unrendered[Document]{
+class MessageBuffer extends ArrayBuffer[Document] with Unrendered[Document]{
   override def addUnrendered (id: Int, m: Document) {
-    update(id, m)
+    append(m)
   }
   override def getUnrendered (id: Int): Option[Document] = {
     if(id < size && id >= 0 && apply(id) != null) Some (apply(id))