# HG changeset patch
# User wenzelm
# Date 1754224939 -7200
# Node ID 37efc8611dca76b338da38f531bdfd85ae699ea6
# Parent  05607b3e6e6c6021d7f9d0d7947e76cfd82757c2
avoid duplicate state output (amending 951abf9db857);

diff -r 05607b3e6e6c -r 37efc8611dca 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