# HG changeset patch
# User wenzelm
# Date 1374177635 -7200
# Node ID 51dfdcd88e84cd051aafac5de28859565aa6cef8
# Parent  d63f80f9302531b1dbc55510b2b9415fe8844ba4
guard unify tracing via visible status of global theory;
find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;

diff -r d63f80f93025 -r 51dfdcd88e84 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 21:57:27 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:00:35 2013 +0200
@@ -631,8 +631,18 @@
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;
+            val thy' =
+              Proof_Context.theory_of ctxt
+              |> Theory.copy
+              |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
+              |> Theory.checkpoint;
+
             val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
-          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
+            val (ctxt', opt_goal') =
+              (case opt_goal of
+                NONE => (ctxt, NONE)
+              | SOME th => (Proof_Context.transfer thy' ctxt, SOME (Thm.transfer thy' th)));
+          in print_theorems ctxt' opt_goal' opt_lim rem_dups spec end)));
 
 end;
 
diff -r d63f80f93025 -r 51dfdcd88e84 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Thu Jul 18 21:57:27 2013 +0200
+++ b/src/Pure/unify.ML	Thu Jul 18 22:00:35 2013 +0200
@@ -189,7 +189,10 @@
 fun test_unify_types thy (T, U) env =
   let
     val str_of = Syntax.string_of_typ_global thy;
-    fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
+    fun warn () =
+      if Context_Position.is_visible_global thy then
+        tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T)
+      else ();
     val env' = unify_types thy (T, U) env;
   in if is_TVar T orelse is_TVar U then warn () else (); env' end;
 
@@ -572,14 +575,16 @@
   In t==u print u first because it may be rigid or flexible --
     t is always flexible.*)
 fun print_dpairs thy msg (env, dpairs) =
-  let
-    fun pdp (rbinder, t, u) =
-      let
-        fun termT t =
-          Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
-        val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t];
-      in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
-  in tracing msg; List.app pdp dpairs end;
+  if Context_Position.is_visible_global thy then
+    let
+      fun pdp (rbinder, t, u) =
+        let
+          fun termT t =
+            Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
+          val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t];
+        in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
+    in tracing msg; List.app pdp dpairs end
+  else ();
 
 
 (*Unify the dpairs in the environment.
@@ -602,7 +607,8 @@
             [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
           | dp :: frigid' =>
               if tdepth > search_bound then
-                (warning "Unification bound exceeded"; Seq.pull reseq)
+                (Context_Position.if_visible_global thy warning "Unification bound exceeded";
+                 Seq.pull reseq)
               else
                (if tdepth > trace_bound then
                   print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
@@ -611,8 +617,8 @@
                     (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
         end
         handle CANTUNIFY =>
-         (if tdepth > trace_bound then tracing "Failure node" else ();
-          Seq.pull reseq));
+         (if tdepth > trace_bound then Context_Position.if_visible_global thy tracing "Failure node"
+          else (); Seq.pull reseq));
     val dps = map (fn (t, u) => ([], t, u)) tus;
   in add_unify 1 ((env, dps), Seq.empty) end;
 
diff -r d63f80f93025 -r 51dfdcd88e84 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Thu Jul 18 21:57:27 2013 +0200
+++ b/src/Tools/solve_direct.ML	Thu Jul 18 22:00:35 2013 +0200
@@ -29,6 +29,7 @@
 val noneN = "none";
 val unknownN = "none";
 
+
 (* preferences *)
 
 val max_solutions = Unsynchronized.ref 5;
@@ -46,10 +47,11 @@
 fun do_solve_direct mode state =
   let
     val ctxt = Proof.context_of state;
+    val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt;
 
     val crits = [(true, Find_Theorems.Solves)];
     fun find g =
-      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
+      snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits);
 
     fun prt_result (goal, results) =
       let