--- a/src/Pure/Thy/sessions.scala Wed Apr 13 16:46:05 2016 +0200
+++ b/src/Pure/Thy/sessions.scala Wed Apr 13 17:00:02 2016 +0200
@@ -167,7 +167,7 @@
(CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
- private object Parser extends Parse.Parser
+ private object Parser extends Parse.Parser with Options.Parser
{
private abstract class Entry
private sealed case class Chapter(name: String) extends Entry
@@ -195,7 +195,8 @@
val session_name = atom("session name", _.is_name)
val option =
- name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+ option_name ~ opt($$$("=") ~! option_value ^^
+ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
val theories =