src/Pure/General/linear_set.scala
changeset 34304 b32c68328d24
parent 34301 78c10aea025d
child 36011 3ff725ac13a4
equal deleted inserted replaced
34303:98425e77cfeb 34304:b32c68328d24
   116   def empty[B]: Linear_Set[B] = Linear_Set.empty
   116   def empty[B]: Linear_Set[B] = Linear_Set.empty
   117 
   117 
   118   override def isEmpty: Boolean = !rep.first.isDefined
   118   override def isEmpty: Boolean = !rep.first.isDefined
   119   def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   119   def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   120 
   120 
   121   def elements: Iterator[A] = new Iterator[A] {
   121   def contains(elem: A): Boolean =
   122     private var next_elem = rep.first
   122     !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
       
   123 
       
   124   private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
       
   125     private var next_elem = start
   123     def hasNext = next_elem.isDefined
   126     def hasNext = next_elem.isDefined
   124     def next =
   127     def next =
   125       next_elem match {
   128       next_elem match {
   126         case Some(elem) =>
   129         case Some(elem) =>
   127           next_elem = rep.nexts.get(elem)
   130           next_elem = rep.nexts.get(elem)
   128           elem
   131           elem
   129         case None => throw new NoSuchElementException("next on empty iterator")
   132         case None => throw new NoSuchElementException("next on empty iterator")
   130       }
   133       }
   131   }
   134   }
   132 
   135 
   133   def contains(elem: A): Boolean =
   136   def elements: Iterator[A] = elements_from(rep.first)
   134     !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
   137 
       
   138   def elements(elem: A): Iterator[A] =
       
   139     if (contains(elem)) elements_from(Some(elem))
       
   140     else throw new Linear_Set.Undefined(elem.toString)
   135 
   141 
   136   def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
   142   def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
   137 
   143 
   138   override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
   144   override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
   139     this + elem1 + elem2 ++ elems
   145     this + elem1 + elem2 ++ elems