# HG changeset patch
# User wenzelm
# Date 1274735980 -7200
# Node ID 5e42e36a6693c903134fd49b6c175bfd24452577
# Parent  9105c8237c7a41b8219b5022b551778560e69ebc
@tailrec annotation;

diff -r 9105c8237c7a -r 5e42e36a6693 src/Pure/PIDE/document.scala
--- 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) =>