src/Pure/Isar/parse.scala

--- a/src/Pure/Isar/parse.scala	Thu Aug 23 17:46:03 2012 +0200
+++ b/src/Pure/Isar/parse.scala	Thu Aug 23 19:57:55 2012 +0200
@@ -44,9 +44,6 @@
       }
     }
 
-    def not_eof: Parser[Elem] = token("input token", _ => true)
-    def eof: Parser[Unit] = not(not_eof)
-
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
       token(s, pred) ^^ (_.content)
 
@@ -79,8 +76,14 @@
     /* 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(p <~ eof, in)
+    {
+      val result = parse(p, in)
+      val rest = proper(result.next)
+      if (result.successful && !rest.atEnd) Error("bad input", rest)
+      else result
+    }
   }
 }