src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Wed Nov 05 21:59:21 2014 +0100
+++ b/src/Pure/System/options.scala	Wed Nov 05 22:17:05 2014 +0100
@@ -93,15 +93,15 @@
     {
       command(SECTION) ~! text ^^
         { case _ ~ a => (options: Options) => options.set_section(a) } |
-      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
-      keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
+      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~
+      $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
         { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
     }
 
     val prefs_entry: Parser[Options => Options] =
     {
-      option_name ~ (keyword("=") ~! option_value) ^^
+      option_name ~ ($$$("=") ~! option_value) ^^
       { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
     }