improved errors of parser combinators;
authorwenzelm
Thu Aug 23 19:57:55 2012 +0200 (2012-08-23)
changeset 48912ffdb37019b2f
parent 48911 5debc3e4fa81
child 48913 f686cb016c0c
improved errors of parser combinators;
src/Pure/Isar/parse.scala
src/Pure/System/build.scala
     1.1 --- a/src/Pure/Isar/parse.scala	Thu Aug 23 17:46:03 2012 +0200
     1.2 +++ b/src/Pure/Isar/parse.scala	Thu Aug 23 19:57:55 2012 +0200
     1.3 @@ -44,9 +44,6 @@
     1.4        }
     1.5      }
     1.6  
     1.7 -    def not_eof: Parser[Elem] = token("input token", _ => true)
     1.8 -    def eof: Parser[Unit] = not(not_eof)
     1.9 -
    1.10      def atom(s: String, pred: Elem => Boolean): Parser[String] =
    1.11        token(s, pred) ^^ (_.content)
    1.12  
    1.13 @@ -79,8 +76,14 @@
    1.14      /* wrappers */
    1.15  
    1.16      def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
    1.17 +
    1.18      def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] =
    1.19 -      parse(p <~ eof, in)
    1.20 +    {
    1.21 +      val result = parse(p, in)
    1.22 +      val rest = proper(result.next)
    1.23 +      if (result.successful && !rest.atEnd) Error("bad input", rest)
    1.24 +      else result
    1.25 +    }
    1.26    }
    1.27  }
    1.28  
     2.1 --- a/src/Pure/System/build.scala	Thu Aug 23 17:46:03 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Thu Aug 23 19:57:55 2012 +0200
     2.3 @@ -177,15 +177,18 @@
     2.4          keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
     2.5            { case _ ~ (x ~ y) => (x, y) }
     2.6  
     2.7 -      ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
     2.8 -        (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
     2.9 -        (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~
    2.10 -        (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
    2.11 -        (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
    2.12 -        (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
    2.13 -        rep(theories) ~
    2.14 -        (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
    2.15 -          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) }
    2.16 +      command(SESSION) ~!
    2.17 +        (session_name ~
    2.18 +          ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
    2.19 +          ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
    2.20 +          (keyword("=") ~!
    2.21 +            (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
    2.22 +              ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    2.23 +              ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    2.24 +              rep(theories) ~
    2.25 +              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
    2.26 +        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
    2.27 +            Session_Entry(pos, a, b, c, d, e, f, g, h) }
    2.28      }
    2.29  
    2.30      def parse_entries(root: Path): List[Session_Entry] =