175 |
175 |
176 val theories = |
176 val theories = |
177 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^ |
177 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^ |
178 { case _ ~ (x ~ y) => (x, y) } |
178 { case _ ~ (x ~ y) => (x, y) } |
179 |
179 |
180 ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ |
180 command(SESSION) ~! |
181 (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~ |
181 (session_name ~ |
182 (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~ |
182 ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ |
183 (keyword("=") ~> opt(session_name <~ keyword("+"))) ~ |
183 ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~ |
184 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~ |
184 (keyword("=") ~! |
185 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~ |
185 (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~ |
186 rep(theories) ~ |
186 ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ |
187 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^ |
187 ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ |
188 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) } |
188 rep(theories) ~ |
|
189 ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^ |
|
190 { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) => |
|
191 Session_Entry(pos, a, b, c, d, e, f, g, h) } |
189 } |
192 } |
190 |
193 |
191 def parse_entries(root: Path): List[Session_Entry] = |
194 def parse_entries(root: Path): List[Session_Entry] = |
192 { |
195 { |
193 val toks = root_syntax.scan(File.read(root)) |
196 val toks = root_syntax.scan(File.read(root)) |