# HG changeset patch # User wenzelm # Date 1345744675 -7200 # Node ID ffdb37019b2f85b04b4f50f32b5054e8ffda00f8 # Parent 5debc3e4fa81f1e6e4485774dc028beb0d79e858 improved errors of parser combinators; diff -r 5debc3e4fa81 -r ffdb37019b2f 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 + } } } diff -r 5debc3e4fa81 -r ffdb37019b2f src/Pure/System/build.scala --- 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] =