# HG changeset patch
# User wenzelm
# Date 1623058925 -7200
# Node ID 72900f34dbb3e66f5c2fab244de4fd621c1fb2b5
# Parent  5b49c650d413957f199120afbdd6a5087342592b
allow system option short form NAME for NAME=true for type string, not just bool;
support short system options "-o document" and "-o system_log";

diff -r 5b49c650d413 -r 72900f34dbb3 NEWS
--- a/NEWS	Mon Jun 07 09:36:21 2021 +0200
+++ b/NEWS	Mon Jun 07 11:42:05 2021 +0200
@@ -232,9 +232,15 @@
 *** System ***
 
 * System option "system_log" specifies an optional log file for internal
-messages produced by Output.system_message in Isabelle/ML; "-" refers to
-console progress of the build job. This works for "isabelle build" or
-any derivative of it.
+messages produced by Output.system_message in Isabelle/ML; the value
+"true" 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). More options.
diff -r 5b49c650d413 -r 72900f34dbb3 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Mon Jun 07 09:36:21 2021 +0200
+++ b/src/Doc/System/Presentation.thy	Mon Jun 07 11:42:05 2021 +0200
@@ -47,9 +47,9 @@
   reported by the above verbose invocation of the build process.
 
   Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
-  \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are
+  \<^dir>\<open>~~/src/HOL/Library\<close>) also provide theory documents in PDF. These are
   prepared automatically as well if enabled like this:
-  @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
+  @{verbatim [display] \<open>isabelle build -o browser_info -o document -v -c HOL-Library\<close>}
 
   Enabling both browser info and document preparation simultaneously causes an
   appropriate ``document'' link to be included in the HTML index. Documents
diff -r 5b49c650d413 -r 72900f34dbb3 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Jun 07 09:36:21 2021 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Jun 07 11:42:05 2021 +0200
@@ -201,8 +201,9 @@
     info, see also \secref{sec:info}.
 
     \<^item> @{system_option_def "document"} controls document output for a
-    particular session or theory; \<^verbatim>\<open>document=pdf\<close> means enabled,
-    \<^verbatim>\<open>document=false\<close> means disabled (especially for particular theories).
+    particular session or theory; \<^verbatim>\<open>document=pdf\<close> or \<^verbatim>\<open>document=true\<close> means
+    enabled, \<^verbatim>\<open>document=""\<close> or \<^verbatim>\<open>document=false\<close> means disabled (especially
+    for particular theories).
 
     \<^item> @{system_option_def "document_output"} specifies an alternative
     directory for generated output of the document preparation system; the
@@ -278,7 +279,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; ``\<^verbatim>\<open>-\<close>'' refers to console progress of the build job.
+    Isabelle/ML; the value ``\<^verbatim>\<open>true\<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
@@ -410,11 +412,12 @@
   The build process depends on additional options
   (\secref{sec:system-options}) that are passed to the prover eventually. The
   settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
-  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
-  Moreover, the environment of system build options may be augmented on the
-  command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates
-  \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
-  the command-line are applied in the given order.
+  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
+  threads=4"\<close>. Moreover, the environment of system build options may be
+  augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>,
+  which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean or string options.
+  Multiple occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given
+  order.
 
   \<^medskip>
   Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where
@@ -496,7 +499,7 @@
 
   \<^smallskip>
   Build all sessions with HTML browser info and PDF document preparation:
-  @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
+  @{verbatim [display] \<open>isabelle build -a -o browser_info -o document\<close>}
 
   \<^smallskip>
   Build all sessions with a maximum of 8 parallel prover processes and 4
diff -r 5b49c650d413 -r 72900f34dbb3 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Jun 07 09:36:21 2021 +0200
+++ b/src/Pure/System/options.scala	Mon Jun 07 11:42:05 2021 +0200
@@ -349,7 +349,7 @@
     val opt = check_name(name)
     opt_value match {
       case Some(value) => this + (name, value)
-      case None if opt.typ == Options.Bool => this + (name, "true")
+      case None if opt.typ == Options.Bool | opt.typ == Options.String => this + (name, "true")
       case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
     }
   }
diff -r 5b49c650d413 -r 72900f34dbb3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jun 07 09:36:21 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Jun 07 11:42:05 2021 +0200
@@ -510,7 +510,7 @@
     def document_enabled: Boolean =
       options.string("document") match {
         case "" | "false" => false
-        case "pdf" => true
+        case "pdf" | "true" => true
         case doc => error("Bad document specification " + quote(doc))
       }
 
diff -r 5b49c650d413 -r 72900f34dbb3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jun 07 09:36:21 2021 +0200
+++ b/src/Pure/Tools/build.scala	Mon Jun 07 11:42:05 2021 +0200
@@ -296,7 +296,7 @@
     val log =
       build_options.string("system_log") match {
         case "" => No_Logger
-        case "-" => Logger.make(progress)
+        case "true" => Logger.make(progress)
         case log_file => Logger.make(Some(Path.explode(log_file)))
       }