# HG changeset patch
# User wenzelm
# Date 1263163405 -3600
# Node ID b32c68328d24e26844a38a37bb999ae13643baf4
# Parent  98425e77cfeb74bd0b43fc763de89e6c106e862a
elements with start entry;

diff -r 98425e77cfeb -r b32c68328d24 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sun Jan 10 23:16:26 2010 +0100
+++ b/src/Pure/General/linear_set.scala	Sun Jan 10 23:43:25 2010 +0100
@@ -118,8 +118,11 @@
   override def isEmpty: Boolean = !rep.first.isDefined
   def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
-  def elements: Iterator[A] = new Iterator[A] {
-    private var next_elem = rep.first
+  def contains(elem: A): Boolean =
+    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+
+  private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+    private var next_elem = start
     def hasNext = next_elem.isDefined
     def next =
       next_elem match {
@@ -130,8 +133,11 @@
       }
   }
 
-  def contains(elem: A): Boolean =
-    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+  def elements: Iterator[A] = elements_from(rep.first)
+
+  def elements(elem: A): Iterator[A] =
+    if (contains(elem)) elements_from(Some(elem))
+    else throw new Linear_Set.Undefined(elem.toString)
 
   def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)