# HG changeset patch
# User nipkow
# Date 1709027388 -3600
# Node ID 6dbe7910dcfc72cd8b63b90b391335f33bd88024
# Parent  4031aafc2ddac08a6de2d12ffb3f8f0701097bd4
simplifier: no trace info from simprocs unless simp_debug = true.

diff -r 4031aafc2dda -r 6dbe7910dcfc src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Feb 26 13:10:37 2024 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Tue Feb 27 10:49:48 2024 +0100
@@ -743,8 +743,8 @@
   Simplifier tracing and debugging.
 
   \<^descr> @{attribute simp_trace} makes the Simplifier output internal operations.
-  This includes rewrite steps, but also bookkeeping like modifications of the
-  simpset.
+  This includes rewrite steps (but not traces from simproc calls),
+  but also bookkeeping like modifications of the simpset.
 
   \<^descr> @{attribute simp_trace_depth_limit} limits the effect of @{attribute
   simp_trace} to the given depth of recursive Simplifier invocations (when
@@ -752,7 +752,7 @@
 
   \<^descr> @{attribute simp_debug} makes the Simplifier output some extra information
   about internal operations. This includes any attempted invocation of
-  simplification procedures.
+  simplification procedures and the corresponding traces.
 
   \<^descr> @{attribute simp_trace_new} controls Simplifier tracing within
   Isabelle/PIDE applications, notably Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>.
diff -r 4031aafc2dda -r 6dbe7910dcfc src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon Feb 26 13:10:37 2024 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Feb 27 10:49:48 2024 +0100
@@ -1057,19 +1057,21 @@
           if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
             (cond_tracing' ctxt simp_debug (fn () =>
               print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
-             (case Morphism.form_context' ctxt proc eta_t' of
-               NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
-             | SOME raw_thm =>
-                 (cond_tracing ctxt (fn () =>
-                    print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:")
-                      ("", raw_thm));
-                  (case rews (mk_procrule ctxt raw_thm) of
-                    NONE =>
-                     (cond_tracing ctxt (fn () =>
-                        print_term ctxt ("IGNORED result of simproc " ^ quote name ^
-                            " -- does not match") (Thm.term_of t));
-                      proc_rews ps)
-                  | some => some))))
+             (let val ctxt' = Config.put simp_trace (Config.get ctxt simp_debug) ctxt
+              in case Morphism.form_context' ctxt' proc eta_t' of
+                NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
+              | SOME raw_thm =>
+                  (cond_tracing ctxt (fn () =>
+                     print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:")
+                       ("", raw_thm));
+                   (case rews (mk_procrule ctxt raw_thm) of
+                     NONE =>
+                      (cond_tracing ctxt (fn () =>
+                         print_term ctxt ("IGNORED result of simproc " ^ quote name ^
+                             " -- does not match") (Thm.term_of t));
+                       proc_rews ps)
+                   | some => some))
+              end))
           else proc_rews ps;
   in
     (case eta_t of