clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";

--- a/NEWS	Sat Nov 20 20:42:41 2021 +0100
+++ b/NEWS	Sun Nov 21 17:42:11 2021 +0100
@@ -548,17 +548,21 @@
 INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
 https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
 
+* System options may declare an implicit standard value, which is used
+when the option is activated without providing an explicit value, e.g.
+"isabelle build -o document -o document_output" instead of
+"isabelle build -o document=true -o document_output=output". For options
+of type "bool", the standard is always "true" and cannot be specified
+differently.
+
+* System option "document=true" is an alias for "document=pdf", and
+"document=false" is an alias for "document=" (empty string).
+
 * System option "system_log" specifies an optional log file for internal
-messages produced by Output.system_message in Isabelle/ML; the value
-"true" refers to console progress of the build job. This works for
+messages produced by Output.system_message in Isabelle/ML; the standard
+value "-" refers to console progress of the build job. This works for
 "isabelle build" or any derivative of it.
 
-* System options of type string may be set to "true" using the short
-notation of type bool. E.g. "isabelle build -o system_log".
-
-* System option "document=true" is an alias for "document=pdf" and thus
-can be used in the short form. E.g. "isabelle build -o document".
-
 * Command-line tool "isabelle version" supports repository archives
 (without full .hg directory). It also provides more options.
 

--- a/etc/options	Sat Nov 20 20:42:41 2021 +0100
+++ b/etc/options	Sun Nov 21 17:42:11 2021 +0100
@@ -5,9 +5,9 @@
 option browser_info : bool = false
   -- "generate theory browser information"
 
-option document : string = ""
+option document : string = "" (standard "true")
   -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
-option document_output : string = ""
+option document_output : string = "" (standard "output")
   -- "document output directory"
 option document_echo : bool = false
   -- "inform about document file names during session presentation"
@@ -17,11 +17,11 @@
   -- "default command tags (separated by commas)"
 option document_bibliography : bool = false
   -- "explicitly enable use of bibtex (default: according to presence of root.bib)"
-option document_build : string = "lualatex"
-  -- "document build engine (e.g. lualatex, pdflatex, build)"
+option document_build : string = "lualatex" (standard "build")
+  -- "document build engine (e.g. build, lualatex, pdflatex)"
 option document_logo : string = ""
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
-option document_heading_prefix : string = "isamarkup"
+option document_heading_prefix : string = "isamarkup" (standard)
   -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
 
 option thy_output_display : bool = false
@@ -130,11 +130,11 @@
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
-option profiling : string = ""
+option profiling : string = "" (standard "time")
   -- "ML profiling (possible values: time, allocations)"
 
-option system_log : string = ""
-  -- "output for system messages (log file or \"true\" for console progress)"
+option system_log : string = "" (standard "-")
+  -- "output for system messages (log file or \"-\" for console progress)"
 
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"

--- a/src/Doc/System/Sessions.thy	Sat Nov 20 20:42:41 2021 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Nov 21 17:42:11 2021 +0100
@@ -273,8 +273,8 @@
 
     \<^item> @{system_option_def system_log} specifies an optional log file for
     low-level messages produced by \<^ML>\<open>Output.system_message\<close> in
-    Isabelle/ML; the value ``\<^verbatim>\<open>true\<close>'' refers to console progress of the build
-    job.
+    Isabelle/ML; the standard value ``\<^verbatim>\<open>-\<close>'' refers to console progress of the
+    build job.
 
     \<^item> @{system_option_def "system_heaps"} determines the directories for
     session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and

--- a/src/Pure/System/options.scala	Sat Nov 20 20:42:41 2021 +0100
+++ b/src/Pure/System/options.scala	Sun Nov 21 17:42:11 2021 +0100
@@ -33,14 +33,21 @@
     typ: Type,
     value: String,
     default_value: String,
+    standard_value: Option[String],
     description: String,
     section: String)
   {
+    private def print_value(x: String): String = if (typ == Options.String) quote(x) else x
+    private def print_standard: String =
+      standard_value match {
+        case None => ""
+        case Some(s) if s == default_value => " (standard)"
+        case Some(s) => " (standard " + print_value(s) + ")"
+      }
     private def print(default: Boolean): String =
     {
       val x = if (default) default_value else value
-      "option " + name + " : " + typ.print + " = " +
-        (if (typ == Options.String) quote(x) else x) +
+      "option " + name + " : " + typ.print + " = " + print_value(x) + print_standard +
         (if (description == "") "" else "\n  -- " + quote(description))
     }
 
@@ -67,14 +74,17 @@
   private val SECTION = "section"
   private val PUBLIC = "public"
   private val OPTION = "option"
+  private val STANDARD = "standard"
   private val OPTIONS = Path.explode("etc/options")
   private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
 
   val options_syntax: Outer_Syntax =
-    Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
+    Outer_Syntax.empty + ":" + "=" + "--" + "(" + ")" +
+      Symbol.comment + Symbol.comment_decoded +
       (SECTION, Keyword.DOCUMENT_HEADING) +
       (PUBLIC, Keyword.BEFORE_COMMAND) +
-      (OPTION, Keyword.THY_DECL)
+      (OPTION, Keyword.THY_DECL) +
+      STANDARD
 
   val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "="
 
@@ -86,6 +96,8 @@
       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)
+    val option_standard: Parser[Option[String]] =
+      $$$("(") ~! $$$(STANDARD) ~ opt(option_value) ~ $$$(")") ^^ { case _ ~ _ ~ a ~ _ => a }
   }
 
   private object Parser extends Parser
@@ -98,9 +110,10 @@
       command(SECTION) ~! text ^^
         { case _ ~ a => (options: Options) => options.set_section(a) } |
       opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
-      $$$("=") ~ option_value ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^
-        { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
-            (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
+      $$$("=") ~ option_value ~ opt(option_standard) ~
+        (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^
+        { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e ~ f) =>
+            (options: Options) => options.declare(a.isDefined, pos, b, c, d, e, f) }
     }
 
     val prefs_entry: Parser[Options => Options] =
@@ -302,6 +315,7 @@
     name: String,
     typ_name: String,
     value: String,
+    standard: Option[Option[String]],
     description: String): Options =
   {
     options.get(name) match {
@@ -319,7 +333,16 @@
               error("Unknown type for option " + quote(name) + " : " + quote(typ_name) +
                 Position.here(pos))
           }
-        val opt = Options.Opt(public, pos, name, typ, value, value, description, section)
+        val standard_value =
+          standard match {
+            case None => None
+            case Some(_) if typ == Options.Bool =>
+              error("Illegal standard value for option " + quote(name) + " : " + typ_name +
+                Position.here)
+            case Some(s) => Some(s.getOrElse(value))
+          }
+        val opt =
+          Options.Opt(public, pos, name, typ, value, value, standard_value, description, section)
         (new Options(options + (name -> opt), section)).check_value(name)
     }
   }
@@ -328,7 +351,7 @@
   {
     if (options.isDefinedAt(name)) this + (name, value)
     else {
-      val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "")
+      val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, None, "", "")
       new Options(options + (name -> opt), section)
     }
   }
@@ -342,9 +365,9 @@
   def + (name: String, opt_value: Option[String]): Options =
   {
     val opt = check_name(name)
-    opt_value match {
+    opt_value orElse opt.standard_value match {
       case Some(value) => this + (name, value)
-      case None if opt.typ == Options.Bool | opt.typ == Options.String => this + (name, "true")
+      case None if opt.typ == Options.Bool => this + (name, "true")
       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
     }
   }

--- a/src/Pure/Tools/build.scala	Sat Nov 20 20:42:41 2021 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 21 17:42:11 2021 +0100
@@ -305,7 +305,7 @@
     val log =
       build_options.string("system_log") match {
         case "" => No_Logger
-        case "true" => Logger.make(progress)
+        case "-" => Logger.make(progress)
         case log_file => Logger.make(Some(Path.explode(log_file)))
       }