# HG changeset patch
# User wenzelm
# Date 1662461042 -7200
# Node ID 951abf9db8578c50d474e71403b96837138d2366
# Parent  5fc4e1fc39b155f09aaa4903c0f3594400a13d91
option "show_states" for more verbosity of batch-builds;

diff -r 5fc4e1fc39b1 -r 951abf9db857 NEWS
--- a/NEWS	Tue Sep 06 12:40:36 2022 +0200
+++ b/NEWS	Tue Sep 06 12:44:02 2022 +0200
@@ -21,6 +21,21 @@
   - "chapter_definition NAME description TEXT" to provide a description
   for presentation purposes
 
+* System option "show_states" controls output of toplevel command states
+(notably proof states) in batch-builds; in interactive mode this is
+always done on demand. The option is relevant for tools that operate on
+exported PIDE markup, e.g. document presentation or diagnostics. For
+example:
+
+  isabelle build -o show_states FOL-ex
+  isabelle log -v -U FOL-ex
+
+Option "show_states" is also the default for the configuration option
+"show_results" within the formal context.
+
+Note that printing intermediate states may cause considerable slowdown
+in building a session.
+
 
 *** Isabelle/VSCode Prover IDE ***
 
diff -r 5fc4e1fc39b1 -r 951abf9db857 etc/options
--- a/etc/options	Tue Sep 06 12:40:36 2022 +0200
+++ b/etc/options	Tue Sep 06 12:44:02 2022 +0200
@@ -66,6 +66,10 @@
 option goals_limit : int = 10
   -- "maximum number of subgoals to be printed"
 
+option show_states : bool = false
+  -- "show toplevel states even if outside of interactive mode"
+
+
 option names_long : bool = false
   -- "show fully qualified names"
 option names_short : bool = false
diff -r 5fc4e1fc39b1 -r 951abf9db857 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 06 12:40:36 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 06 12:44:02 2022 +0200
@@ -328,7 +328,9 @@
 
 val show_results =
   Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
-    (fn context => Config.get_generic context interactive);
+    (fn context =>
+      Config.get_generic context interactive orelse
+      Options.default_bool \<^system_option>\<open>show_states\<close>);
 
 fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
 
diff -r 5fc4e1fc39b1 -r 951abf9db857 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Sep 06 12:40:36 2022 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Sep 06 12:44:02 2022 +0200
@@ -628,10 +628,22 @@
 
 local
 
+fun show_state (st', opt_err) =
+  let
+    val enabled = is_none opt_err andalso Options.default_bool \<^system_option>\<open>show_states\<close>;
+    val opt_err' =
+      if enabled then
+        (case Exn.capture (Output.state o string_of_state) st' of
+          Exn.Exn exn => SOME exn
+        | Exn.Res _ => opt_err)
+      else opt_err;
+  in (st', opt_err') end;
+
 fun app int (tr as Transition {name, markers, trans, ...}) =
   setmp_thread_position tr
     (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans)
-      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
+      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)
+      #> show_state);
 
 in