tuned signature;

--- 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]

--- 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"

--- 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