# HG changeset patch
# User wenzelm
# Date 1460559602 -7200
# Node ID 4e4738698db4755cdaf6d9a3e5d1ef47658db255
# Parent  5e8b1aead28fb0a41c13990713bdb548d6eabb5d
clarified syntax;

diff -r 5e8b1aead28f -r 4e4738698db4 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Apr 13 16:46:05 2016 +0200
+++ b/src/Pure/System/options.scala	Wed Apr 13 17:00:02 2016 +0200
@@ -80,15 +80,18 @@
 
   lazy val prefs_syntax = Outer_Syntax.init() + "="
 
-  object Parser extends Parse.Parser
+  trait Parser extends Parse.Parser
   {
-    val option_name = atom("option name", _.is_xname)
-    val option_type = atom("option type", _.is_ident)
+    val option_name = atom("option name", _.is_name)
+    val option_type = atom("option type", _.is_name)
     val option_value =
       opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
         { case s ~ n => if (s.isDefined) "-" + n else n } |
       atom("option value", tok => tok.is_name || tok.is_float)
+  }
 
+  object Parser extends Parse.Parser with Parser
+  {
     def comment_marker: Parser[String] =
       $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
 
diff -r 5e8b1aead28f -r 4e4738698db4 src/Pure/Thy/sessions.scala
--- 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 =