src/Pure/General/linear_set.scala
changeset 37070 e8906d992b69
parent 36781 a991deb77cbb
child 37072 9105c8237c7a
equal deleted inserted replaced
37069:7d796b72099f 37070:e8906d992b69
   127   override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   127   override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   128 
   128 
   129   def contains(elem: A): Boolean =
   129   def contains(elem: A): Boolean =
   130     !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
   130     !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
   131 
   131 
   132   private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
   132   private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
   133     private var next_elem = start
   133     private var next_elem = start
   134     def hasNext = next_elem.isDefined
   134     def hasNext = next_elem.isDefined
   135     def next =
   135     def next =
   136       next_elem match {
   136       next_elem match {
   137         case Some(elem) =>
   137         case Some(elem) =>
   138           next_elem = rep.nexts.get(elem)
   138           next_elem = which.get(elem)
   139           elem
   139           elem
   140         case None => throw new NoSuchElementException("next on empty iterator")
   140         case None => throw new NoSuchElementException("next on empty iterator")
   141       }
   141       }
   142   }
   142   }
   143 
   143 
   144   override def iterator: Iterator[A] = iterator_from(rep.start)
   144   override def iterator: Iterator[A] = make_iterator(rep.start, rep.nexts)
   145 
   145 
   146   def iterator(elem: A): Iterator[A] =
   146   def iterator(elem: A): Iterator[A] =
   147     if (contains(elem)) iterator_from(Some(elem))
   147     if (contains(elem)) make_iterator(Some(elem), rep.nexts)
       
   148     else throw new Linear_Set.Undefined(elem.toString)
       
   149 
       
   150   def rev_iterator(elem: A): Iterator[A] =
       
   151     if (contains(elem)) make_iterator(Some(elem), rep.prevs)
   148     else throw new Linear_Set.Undefined(elem.toString)
   152     else throw new Linear_Set.Undefined(elem.toString)
   149 
   153 
   150   def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
   154   def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
   151 
   155 
   152   def - (elem: A): Linear_Set[A] =
   156   def - (elem: A): Linear_Set[A] =