src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/options.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -55,7 +55,7 @@
           case word :: rest if word == strip => rest
           case _ => words
         }
-      Word.implode(words1.map(Word.perhaps_capitalize(_)))
+      Word.implode(words1.map(Word.perhaps_capitalize))
     }
 
     def unknown: Boolean = typ == Unknown
@@ -70,19 +70,19 @@
   private val OPTIONS = Path.explode("etc/options")
   private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
 
-  val options_syntax =
+  val options_syntax: Outer_Syntax =
     Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
       (SECTION, Keyword.DOCUMENT_HEADING) +
       (PUBLIC, Keyword.BEFORE_COMMAND) +
       (OPTION, Keyword.THY_DECL)
 
-  val prefs_syntax = Outer_Syntax.empty + "="
+  val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "="
 
   trait Parser extends Parse.Parser
   {
-    val option_name = atom("option name", _.is_name)
-    val option_type = atom("option type", _.is_name)
-    val option_value =
+    val option_name: Parser[String] = atom("option name", _.is_name)
+    val option_type: Parser[String] = atom("option type", _.is_name)
+    val option_value: Parser[String] =
       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)