src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Wed Aug 29 12:21:59 2018 +0200
+++ b/src/Pure/System/options.scala	Wed Aug 29 12:44:17 2018 +0200
@@ -88,7 +88,7 @@
       atom("option value", tok => tok.is_name || tok.is_float)
   }
 
-  object Parser extends Parse.Parser with Parser
+  private object Parser extends Parser
   {
     def comment_marker: Parser[String] =
       $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)