src/Pure/Thy/sessions.scala
changeset 62968 4e4738698db4
parent 62946 9f537dd83677
child 62969 9f394a16c557
--- 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 =