From e51ff591f77039fa28c178d3f0585a69ff3595f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 25 Apr 2017 14:16:10 -0700
Subject: [PATCH] chore(library/type_context): disable all trace messages
 inside type class resolution if trace.class_instances is not set to true

---
 src/library/type_context.cpp | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index a1756897ed..27aa51102a 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -3450,9 +3450,7 @@ struct instance_synthesizer {
         return ensure_no_meta(r);
     }
 
-    optional<expr> operator()(expr const & type) {
-        lean_trace_init_bool("class_instances", get_pp_purify_metavars_name(), false);
-        lean_trace_init_bool("class_instances", get_pp_implicit_name(), true);
+    optional<expr> main(expr const & type) {
         auto r = mk_class_instance_core(type);
         if (r) {
             for (unsigned i = 0; i < m_choices.size(); i++) {
@@ -3462,6 +3460,17 @@ struct instance_synthesizer {
         }
         return r;
     }
+
+    optional<expr> operator()(expr const & type) {
+        if (is_trace_enabled() && !is_trace_class_enabled("class_instances")) {
+            scope_trace_silent scope(true);
+            return main(type);
+        } else {
+            lean_trace_init_bool("class_instances", get_pp_purify_metavars_name(), false);
+            lean_trace_init_bool("class_instances", get_pp_implicit_name(), true);
+            return main(type);
+        }
+    }
 };
 
 static bool depends_on_mvar(expr const & e, buffer<expr> const & mvars) {