# HG changeset patch # User wenzelm # Date 1637512931 -3600 # Node ID c1b5d6e6ff74432b6314ae9e682ccfed55cd91f0 # Parent 0e4d8aa61ad73cb6e924827f28a0d6723419d46c clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true"; diff -r 0e4d8aa61ad7 -r c1b5d6e6ff74 NEWS --- 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. diff -r 0e4d8aa61ad7 -r c1b5d6e6ff74 etc/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" diff -r 0e4d8aa61ad7 -r c1b5d6e6ff74 src/Doc/System/Sessions.thy --- 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>\Output.system_message\ in - Isabelle/ML; the value ``\<^verbatim>\true\'' refers to console progress of the build - job. + Isabelle/ML; the standard value ``\<^verbatim>\-\'' refers to console progress of the + build job. \<^item> @{system_option_def "system_heaps"} determines the directories for session heap images: \<^path>\$ISABELLE_HEAPS\ is the user directory and diff -r 0e4d8aa61ad7 -r c1b5d6e6ff74 src/Pure/System/options.scala --- 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) } } diff -r 0e4d8aa61ad7 -r c1b5d6e6ff74 src/Pure/Tools/build.scala --- 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))) }