--- a/src/Pure/PIDE/document.scala Mon May 24 23:01:51 2010 +0200
+++ b/src/Pure/PIDE/document.scala Mon May 24 23:19:40 2010 +0200
@@ -7,6 +7,9 @@
package isabelle
+import scala.annotation.tailrec
+
+
object Document
{
/* command start positions */
@@ -80,7 +83,7 @@
/* phase 2: recover command spans */
- def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+ @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
{
commands.iterator.find(is_unparsed) match {
case Some(first_unparsed) =>