clarified show_results to serve as guard for interactive mode -- avoid printing internal consts, e.g. in 'record' or 'datatype', where Specification.definition is used as convenience for class instantiation (see also 889d5cdc034b, 951abf9db857, ecf80e37ed1a);

--- a/src/Pure/Isar/proof_display.ML	Thu Aug 28 13:49:52 2025 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Aug 28 15:55:07 2025 +0200
@@ -300,7 +300,7 @@
 val show_results =
   Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
     (fn context =>
-      Config.get_generic context interactive orelse
+      Config.get_generic context interactive andalso
       Options.default_bool \<^system_option>\<open>show_results\<close>);
 
 fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);

--- a/src/Pure/Isar/toplevel.ML	Thu Aug 28 13:49:52 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 28 15:55:07 2025 +0200
@@ -659,8 +659,6 @@
       if Exn.is_interrupt_proper exn then Exn.reraise exn
       else raise Runtime.EXCURSION_FAIL (exn, info));
 
-val command = command_exception false;
-
 end;
 
 
@@ -739,6 +737,9 @@
 val empty_markers = markers [];
 val empty_trans = reset_trans #> keep (K ());
 
+fun command tr st =
+  command_exception (Options.default_bool \<^system_option>\<open>show_results\<close>) tr st;
+
 in
 
 fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans);