src/Pure/Isar/outer_parse.scala

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