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;
--- 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;
--- 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;
--- 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