# HG changeset patch
# User wenzelm
# Date 1394207442 -3600
# Node ID 36fd4981c119e295f374890794835f00ef7ccc4b
# Parent  06cb126f30ba7a5059e703f1a7c230b349953071
tuned;

diff -r 06cb126f30ba -r 36fd4981c119 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Mar 07 16:00:45 2014 +0100
+++ b/src/Pure/General/scan.scala	Fri Mar 07 16:50:42 2014 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.{IndexedSeq, TraversableOnce}
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
@@ -323,14 +324,15 @@
     private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
     {
       val len = str.length
-      def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
+      @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
       {
         if (i < len) {
           tree.branches.get(str.charAt(i)) match {
             case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
             case None => None
           }
-        } else Some(tip, tree)
+        }
+        else Some(tip, tree)
       }
       look(rep, false, 0)
     }