1.1 --- a/src/Pure/General/linear_set.scala	Sat Jan 09 23:22:56 2010 +0100
     1.2 +++ b/src/Pure/General/linear_set.scala	Sun Jan 10 17:29:09 2010 +0100
     1.3 @@ -118,14 +118,16 @@
     1.4    override def isEmpty: Boolean = !rep.first.isDefined
     1.5    def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
     1.6  
     1.7 -  def elements = new Iterator[A] {
     1.8 +  def elements: Iterator[A] = new Iterator[A] {
     1.9      private var next_elem = rep.first
    1.10      def hasNext = next_elem.isDefined
    1.11 -    def next = {
    1.12 -      val elem = next_elem.get
    1.13 -      next_elem = rep.nexts.get(elem)
    1.14 -      elem
    1.15 -    }
    1.16 +    def next =
    1.17 +      next_elem match {
    1.18 +        case Some(elem) =>
    1.19 +          next_elem = rep.nexts.get(elem)
    1.20 +          elem
    1.21 +        case None => throw new NoSuchElementException("next on empty iterator")
    1.22 +      }
    1.23    }
    1.24  
    1.25    def contains(elem: A): Boolean =

     2.1 --- a/src/Pure/General/scan.scala	Sat Jan 09 23:22:56 2010 +0100
     2.2 +++ b/src/Pure/General/scan.scala	Sun Jan 10 17:29:09 2010 +0100
     2.3 @@ -108,6 +108,7 @@
     2.4      def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
     2.5  
     2.6  
     2.7 +
     2.8      /** RegexParsers methods **/
     2.9  
    2.10      override val whiteSpace = "".r