--- 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 ***
--- 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
--- 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);
--- 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