avoid duplicate state output (amending 951abf9db857);
authorwenzelm
Sun, 03 Aug 2025 14:42:19 +0200
changeset 82944 37efc8611dca
parent 82943 05607b3e6e6c
child 82945 634b8a0f2966
avoid duplicate state output (amending 951abf9db857);
src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Aug 03 14:29:20 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Aug 03 14:42:19 2025 +0200
@@ -615,9 +615,12 @@
 
 local
 
-fun show_state (st', opt_err) =
+fun show_state tr (st', opt_err) =
   let
-    val enabled = is_none opt_err andalso Options.default_bool \<^system_option>\<open>show_states\<close>;
+    val enabled =
+      not (is_ignored tr) andalso
+      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 Pretty.strings_of o Pretty.chunks o pretty_state) st' of
@@ -630,7 +633,7 @@
   setmp_thread_position tr
     (Timing.protocol (name_of tr) (pos_of tr) (apply_capture int name markers trans)
       ##> Option.map (fn Runtime.UNDEF => ERROR (type_error tr) | exn => exn)
-      #> show_state);
+      #> show_state tr);
 
 fun command_transition int tr st =
   let