src/Pure/Tools/build.scala
changeset 59811 6b0d9e8ac227
parent 59736 5c1a0069b9d3
child 59891 9ce697050455
equal deleted inserted replaced
59810:e749a0f2f401 59811:6b0d9e8ac227
   240         $$$(DOCUMENT_FILES) ~!
   240         $$$(DOCUMENT_FILES) ~!
   241           (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
   241           (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
   242               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
   242               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
   243             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
   243             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
   244 
   244 
   245       position(command(SESSION)) ~!
   245       command(SESSION) ~!
   246         (session_name ~
   246         (position(session_name) ~
   247           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   247           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   248           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   248           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   249           ($$$("=") ~!
   249           ($$$("=") ~!
   250             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
   250             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
   251               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   251               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   252               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   252               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   253               rep1(theories) ~
   253               rep1(theories) ~
   254               (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   254               (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   255               (rep(document_files) ^^ (x => x.flatten))))) ^^
   255               (rep(document_files) ^^ (x => x.flatten))))) ^^
   256         { case (_, pos) ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   256         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   257             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   257             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   258     }
   258     }
   259 
   259 
   260     def parse_entries(root: Path): List[(String, Session_Entry)] =
   260     def parse_entries(root: Path): List[(String, Session_Entry)] =
   261     {
   261     {