# HG changeset patch
# User wenzelm
# Date 1343648680 -7200
# Node ID 305ebcd9018a9010ec6a05399e2d671f79a4bbe8
# Parent  5e64b7770f3501e0bb5e35215d9d435fc601ffbe
proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;

diff -r 5e64b7770f35 -r 305ebcd9018a src/Pure/Isar/parse.scala
--- 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)
   }
 }