Outer_Lex.is_ignored;

--- a/src/Pure/Isar/outer_lex.scala	Mon Jan 11 10:55:43 2010 +0100
+++ b/src/Pure/Isar/outer_lex.scala	Mon Jan 11 18:23:06 2010 +0100
@@ -48,7 +48,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_proper: Boolean = !(is_space || is_comment)
+    def is_ignored: Boolean = is_space || is_comment
     def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
 
     def content: String =

--- a/src/Pure/Isar/outer_parse.scala	Mon Jan 11 10:55:43 2010 +0100
+++ b/src/Pure/Isar/outer_parse.scala	Mon Jan 11 18:23:06 2010 +0100
@@ -20,7 +20,7 @@
     def filter_proper = true
 
     private def proper(in: Input): Input =
-      if (in.atEnd || in.first.is_proper || !filter_proper) in
+      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
       else proper(in.rest)
 
     def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]

--- a/src/Pure/Thy/thy_syntax.scala	Mon Jan 11 10:55:43 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Jan 11 18:23:06 2010 +0100
@@ -15,7 +15,7 @@
 
     val command_span: Parser[Span] =
     {
-      val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
+      val whitespace = token("white space", _.is_ignored)
       val command = token("command keyword", _.is_command)
       val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
       command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)