--- a/NEWS Fri Aug 08 21:28:22 2025 +0200
+++ b/NEWS Sat Aug 09 20:22:19 2025 +0200
@@ -31,9 +31,9 @@
database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
"HOL.Nat" in session "HOL". This information is read-only: editing
theory sources in the editor will invalidate formal markup, and replace
-it by an error message. Output messages exclude proof states and final
-results, unless the underlying session database has been built with
-option "show_states".
+it by an error message. Output messages depend on system options
+"show_results" (default true) and "show_states" (default false),
+provided at build-time for the underlying session database.
*** Isabelle/jEdit Prover IDE ***
@@ -335,6 +335,17 @@
*** System ***
+* System option "show_results" (default true) controls output of
+toplevel command results (definitions, theorems) in batch-builds. In
+interactive mode this is always enabled; in batch-builds it can be
+disable like this:
+
+ isabelle build -o show_results=false FOL
+
+Option "show_results" is also the default for the configuration option
+"show_results" within the formal context --- instead of "show_states"
+that was used for this purpose before.
+
* The traditional ML system settings have been reconsidered, and mostly
replaced by ML_Settings in Isabelle/Scala (e.g. via
ML_Settings.system(Options.init())). Potential INCOMPATIBILITY for old
--- a/etc/options Fri Aug 08 21:28:22 2025 +0200
+++ b/etc/options Sat Aug 09 20:22:19 2025 +0200
@@ -69,6 +69,8 @@
option goals_limit : int = 10 for content
-- "maximum number of subgoals to be printed"
+option show_results : bool = true for content
+ -- "show toplevel results even if outside of interactive mode"
option show_states : bool = false for content
-- "show toplevel states even if outside of interactive mode"
--- a/src/Pure/Isar/proof_display.ML Fri Aug 08 21:28:22 2025 +0200
+++ b/src/Pure/Isar/proof_display.ML Sat Aug 09 20:22:19 2025 +0200
@@ -301,7 +301,7 @@
Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
(fn context =>
Config.get_generic context interactive orelse
- Options.default_bool \<^system_option>\<open>show_states\<close>);
+ Options.default_bool \<^system_option>\<open>show_results\<close>);
fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);