equal
deleted
inserted
replaced
1115 |
1115 |
1116 private val chapter_entry: Parser[Chapter_Entry] = |
1116 private val chapter_entry: Parser[Chapter_Entry] = |
1117 command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) } |
1117 command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) } |
1118 |
1118 |
1119 private val session_entry: Parser[Session_Entry] = { |
1119 private val session_entry: Parser[Session_Entry] = { |
1120 val option = |
1120 val options = $$$("[") ~> rep1sep(option_spec, $$$(",")) <~ $$$("]") |
1121 option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^ |
|
1122 { case x ~ y => Options.Spec(x, y) } |
|
1123 val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]") |
|
1124 |
1121 |
1125 val theory_entry = |
1122 val theory_entry = |
1126 position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) } |
1123 position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) } |
1127 |
1124 |
1128 val theories = |
1125 val theories = |