1.1 --- a/src/Pure/Isar/parse.scala	Mon Jul 30 12:08:25 2012 +0200
     1.2 +++ b/src/Pure/Isar/parse.scala	Mon Jul 30 13:42:45 2012 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  import scala.util.parsing.combinator.Parsers
     1.7 +import scala.annotation.tailrec
     1.8  
     1.9  
    1.10  object Parse
    1.11 @@ -17,10 +18,10 @@
    1.12    {
    1.13      type Elem = Token
    1.14  
    1.15 -    def filter_proper = true
    1.16 +    def filter_proper: Boolean = true
    1.17  
    1.18 -    private def proper(in: Input): Input =
    1.19 -      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
    1.20 +    @tailrec private def proper(in: Input): Input =
    1.21 +      if (!filter_proper || in.atEnd || in.first.is_proper) in
    1.22        else proper(in.rest)
    1.23  
    1.24      def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]

     2.1 --- a/src/Pure/Isar/token.scala	Mon Jul 30 12:08:25 2012 +0200
     2.2 +++ b/src/Pure/Isar/token.scala	Mon Jul 30 13:42:45 2012 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4    def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
     2.5    def is_space: Boolean = kind == Token.Kind.SPACE
     2.6    def is_comment: Boolean = kind == Token.Kind.COMMENT
     2.7 -  def is_ignored: Boolean = is_space || is_comment
     2.8 +  def is_proper: Boolean = !is_space && !is_comment
     2.9    def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
    2.10  
    2.11    def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"

     3.1 --- a/src/Pure/PIDE/command.scala	Mon Jul 30 12:08:25 2012 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Mon Jul 30 13:42:45 2012 +0200
     3.3 @@ -128,7 +128,7 @@
     3.4  
     3.5    def is_defined: Boolean = id != Document.no_id
     3.6  
     3.7 -  val is_ignored: Boolean = span.forall(_.is_ignored)
     3.8 +  val is_ignored: Boolean = !span.exists(_.is_proper)
     3.9    val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
    3.10    def is_command: Boolean = !is_ignored && !is_malformed
    3.11