# HG changeset patch
# User wenzelm
# Date 1344534689 -7200
# Node ID ebfe3dd9f3f753bb269808f10b8abaa84b97a6ab
# Parent  9e1b2aafbc7f039b50dc34e406583a76d4909010
tuned signature;

diff -r 9e1b2aafbc7f -r ebfe3dd9f3f7 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Thu Aug 09 19:37:42 2012 +0200
+++ b/src/Pure/General/linear_set.scala	Thu Aug 09 19:51:29 2012 +0200
@@ -152,6 +152,14 @@
     if (contains(elem)) make_iterator(Some(elem))
     else throw new Linear_Set.Undefined(elem)
 
+  def iterator(from: A, to: A): Iterator[A] =
+    if (!contains(to)) throw new Linear_Set.Undefined(to)
+    else
+      nexts.get(to) match {
+        case None => iterator(from)
+        case Some(stop) => iterator(from).takeWhile(_ != stop)
+      }
+
   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
 
   def - (elem: A): Linear_Set[A] =
diff -r 9e1b2aafbc7f -r ebfe3dd9f3f7 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 19:37:42 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 19:51:29 2012 +0200
@@ -209,8 +209,7 @@
         case Some(first_undefined) =>
           val first = bound(commands.reverse, first_undefined)
           val last = bound(commands, first_undefined)
-          val range =
-            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
+          val range = commands.iterator(first, last).toList
 
           val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))