improved errors of parser combinators;

--- 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
+    }
   }
 }
 

--- a/src/Pure/System/build.scala	Thu Aug 23 17:46:03 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Aug 23 19:57:55 2012 +0200
@@ -177,15 +177,18 @@
         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
-      ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
-        (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
-        (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~
-        (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
-        (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
-        (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
-        rep(theories) ~
-        (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
-          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) }
+      command(SESSION) ~!
+        (session_name ~
+          ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
+          ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
+          (keyword("=") ~!
+            (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
+              ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+              ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+              rep(theories) ~
+              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
+        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
+            Session_Entry(pos, a, b, c, d, e, f, g, h) }
     }
 
     def parse_entries(root: Path): List[Session_Entry] =