tuned;
authorwenzelm
Sun, 10 Jan 2010 17:29:09 +0100
changeset 34301 78c10aea025d
parent 34300 3f2e25dc99ab
child 34302 9bb71dfe7314
tuned;
src/Pure/General/linear_set.scala
src/Pure/General/scan.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 =
--- 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