src/Pure/Tools/build.scala
changeset 56464 555f4be59be6
parent 56428 1acf2d76ac23
child 56533 cd8b6d849b6a
     1.1 --- a/src/Pure/Tools/build.scala	Tue Apr 08 12:31:17 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 08 13:24:08 2014 +0200
     1.3 @@ -203,16 +203,14 @@
     1.4  
     1.5    private object Parser extends Parse.Parser
     1.6    {
     1.7 -    def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
     1.8 -
     1.9 -    def chapter(pos: Position.T): Parser[Chapter] =
    1.10 +    val chapter: Parser[Chapter] =
    1.11      {
    1.12        val chapter_name = atom("chapter name", _.is_name)
    1.13  
    1.14        command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
    1.15      }
    1.16  
    1.17 -    def session_entry(pos: Position.T): Parser[Session_Entry] =
    1.18 +    val session_entry: Parser[Session_Entry] =
    1.19      {
    1.20        val session_name = atom("session name", _.is_name)
    1.21  
    1.22 @@ -234,7 +232,7 @@
    1.23                ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.24                rep1(theories) ~
    1.25                ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
    1.26 -        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
    1.27 +        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
    1.28              Session_Entry(pos, a, b, c, d, e, f, g, h) }
    1.29      }
    1.30  
    1.31 @@ -242,7 +240,7 @@
    1.32      {
    1.33        val toks = root_syntax.scan(File.read(root))
    1.34  
    1.35 -      parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
    1.36 +      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
    1.37          case Success(result, _) =>
    1.38            var chapter = chapter_default
    1.39            val entries = new mutable.ListBuffer[(String, Session_Entry)]