src/Pure/System/build.scala
changeset 48484 70898d016538
parent 48482 45137257399a
child 48485 2cbc3d284cd8
equal deleted inserted replaced
48483:9bfb6978eb80 48484:70898d016538
   140         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   140         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   141 
   141 
   142     val session_entry: Parser[Session_Entry] =
   142     val session_entry: Parser[Session_Entry] =
   143     {
   143     {
   144       val session_name = atom("session name", _.is_name)
   144       val session_name = atom("session name", _.is_name)
   145       val theory_name = atom("theory name", _.is_name)
       
   146 
   145 
   147       val option =
   146       val option =
   148         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   147         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   149       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   148       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   150 
   149