# HG changeset patch
# User wenzelm
# Date 1754763739 -7200
# Node ID 889d5cdc034b076580b237e5b5649b269519a266
# Parent  ae65438eec0c6914a0e107a2ff6cea82dc83dd14
explicit option "show_results" for persistent messages;

diff -r ae65438eec0c -r 889d5cdc034b NEWS
--- 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
diff -r ae65438eec0c -r 889d5cdc034b etc/options
--- 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"
 
diff -r ae65438eec0c -r 889d5cdc034b src/Pure/Isar/proof_display.ML
--- 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);