proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;

--- a/src/Pure/Isar/parse.scala	Mon Jul 30 13:42:45 2012 +0200
+++ b/src/Pure/Isar/parse.scala	Mon Jul 30 13:44:40 2012 +0200
@@ -77,7 +77,8 @@
     /* wrappers */
 
     def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
-    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
+    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] =
+      parse(p <~ eof, in)
   }
 }