# HG changeset patch
# User wenzelm
# Date 1282507754 -7200
# Node ID ff7f9510b0d6a2cabe6855ce397e2a3a9c567e1a
# Parent  3a6ce43d99b13dea9f7a37eed73ca377f76cb66d
tuned;

diff -r 3a6ce43d99b1 -r ff7f9510b0d6 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sun Aug 22 20:25:15 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Sun Aug 22 22:09:14 2010 +0200
@@ -143,13 +143,13 @@
 
   private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
     private var next_elem = start
-    def hasNext = next_elem.isDefined
-    def next =
+    def hasNext(): Boolean = next_elem.isDefined
+    def next(): A =
       next_elem match {
         case Some(elem) =>
           next_elem = which.get(elem)
           elem
-        case None => throw new NoSuchElementException("next on empty iterator")
+        case None => Iterator.empty.next()
       }
   }
 
diff -r 3a6ce43d99b1 -r ff7f9510b0d6 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Aug 22 20:25:15 2010 +0200
+++ b/src/Pure/library.scala	Sun Aug 22 22:09:14 2010 +0200
@@ -79,7 +79,7 @@
     def next(): CharSequence =
       state match {
         case Some((s, i)) => { state = next_chunk(i); s }
-        case None => throw new NoSuchElementException("next on empty iterator")
+        case None => Iterator.empty.next()
       }
   }