--- 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] =
--- 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))