src/Pure/Isar/parse.scala

--- a/src/Pure/Isar/parse.scala	Mon Jul 30 12:08:25 2012 +0200
+++ b/src/Pure/Isar/parse.scala	Mon Jul 30 13:42:45 2012 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 import scala.util.parsing.combinator.Parsers
+import scala.annotation.tailrec
 
 
 object Parse
@@ -17,10 +18,10 @@
   {
     type Elem = Token
 
-    def filter_proper = true
+    def filter_proper: Boolean = true
 
-    private def proper(in: Input): Input =
-      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
+    @tailrec private def proper(in: Input): Input =
+      if (!filter_proper || in.atEnd || in.first.is_proper) in
       else proper(in.rest)
 
     def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]