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