src/Tools/jEdit/src/jedit/ScrollerDockable.scala
changeset 34374 b41c1b50e0a9
parent 34371 4a63526bead1
child 34375 71e86ec7e159
equal deleted inserted replaced
34373:2b730e933006 34374:b41c1b50e0a9
   193 }
   193 }
   194 
   194 
   195 
   195 
   196 
   196 
   197 //containing the unrendered messages
   197 //containing the unrendered messages
   198 class MessageBuffer extends HashMap[Int,Document] with Unrendered[Document]{
   198 class MessageBuffer extends ArrayBuffer[Document] with Unrendered[Document]{
   199   override def addUnrendered (id: Int, m: Document) {
   199   override def addUnrendered (id: Int, m: Document) {
   200     update(id, m)
   200     append(m)
   201   }
   201   }
   202   override def getUnrendered (id: Int): Option[Document] = {
   202   override def getUnrendered (id: Int): Option[Document] = {
   203     if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
   203     if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
   204     else None
   204     else None
   205   }
   205   }