# 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))