# HG changeset patch # User wenzelm # Date 1343648565 -7200 # Node ID 5e64b7770f3501e0bb5e35215d9d435fc601ffbe # Parent 7f4561d43d391f14724025376c293c47462bc6de tuned signature; diff -r 7f4561d43d39 -r 5e64b7770f35 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] diff -r 7f4561d43d39 -r 5e64b7770f35 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Mon Jul 30 12:08:25 2012 +0200 +++ b/src/Pure/Isar/token.scala Mon Jul 30 13:42:45 2012 +0200 @@ -86,7 +86,7 @@ def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT - def is_ignored: Boolean = is_space || is_comment + def is_proper: Boolean = !is_space && !is_comment def is_unparsed: Boolean = kind == Token.Kind.UNPARSED def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin" diff -r 7f4561d43d39 -r 5e64b7770f35 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Jul 30 12:08:25 2012 +0200 +++ b/src/Pure/PIDE/command.scala Mon Jul 30 13:42:45 2012 +0200 @@ -128,7 +128,7 @@ def is_defined: Boolean = id != Document.no_id - val is_ignored: Boolean = span.forall(_.is_ignored) + val is_ignored: Boolean = !span.exists(_.is_proper) val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed)) def is_command: Boolean = !is_ignored && !is_malformed