# HG changeset patch
# User wenzelm
# Date 1263140949 -3600
# Node ID 78c10aea025d95847b762698b418b9902485c3fd
# Parent  3f2e25dc99ab91690178bade1b32c96aa933865d
tuned;

diff -r 3f2e25dc99ab -r 78c10aea025d src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/Pure/General/linear_set.scala	Sun Jan 10 17:29:09 2010 +0100
@@ -118,14 +118,16 @@
   override def isEmpty: Boolean = !rep.first.isDefined
   def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
-  def elements = new Iterator[A] {
+  def elements: Iterator[A] = new Iterator[A] {
     private var next_elem = rep.first
     def hasNext = next_elem.isDefined
-    def next = {
-      val elem = next_elem.get
-      next_elem = rep.nexts.get(elem)
-      elem
-    }
+    def next =
+      next_elem match {
+        case Some(elem) =>
+          next_elem = rep.nexts.get(elem)
+          elem
+        case None => throw new NoSuchElementException("next on empty iterator")
+      }
   }
 
   def contains(elem: A): Boolean =
diff -r 3f2e25dc99ab -r 78c10aea025d src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/Pure/General/scan.scala	Sun Jan 10 17:29:09 2010 +0100
@@ -108,6 +108,7 @@
     def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
 
 
+
     /** RegexParsers methods **/
 
     override val whiteSpace = "".r