src/Tools/jEdit/src/utils/LinearSet.scala
changeset 34535 690927d66d8c
parent 34531 db1c28e326fc
child 34538 20bfcca24658
equal deleted inserted replaced
34532:aaafe9c4180b 34535:690927d66d8c
    32 
    32 
    33 
    33 
    34   /* basic methods */
    34   /* basic methods */
    35 
    35 
    36   def next(elem: A) = body.get(elem)
    36   def next(elem: A) = body.get(elem)
    37   
    37   def prev(elem: A) = body.find(_._2 == elem).map(_._2)
    38   override def isEmpty: Boolean = !last_elem.isDefined
    38   override def isEmpty: Boolean = !last_elem.isDefined
    39   def size: Int = if (isEmpty) 0 else body.size + 1
    39   def size: Int = if (isEmpty) 0 else body.size + 1
    40 
    40 
    41   def empty[B] = LinearSet.empty[B]
    41   def empty[B] = LinearSet.empty[B]
    42 
    42