104 (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification |
104 (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification |
105 bound exceeded" warnings and the like. *) |
105 bound exceeded" warnings and the like. *) |
106 fun silence_methods debug = |
106 fun silence_methods debug = |
107 Config.put Metis_Tactic.verbose debug |
107 Config.put Metis_Tactic.verbose debug |
108 #> Config.put Lin_Arith.verbose debug |
108 #> Config.put Lin_Arith.verbose debug |
109 #> (not debug ? |
109 #> not debug ? (fn ctxt => |
110 (Context_Position.set_visible false |
110 ctxt |
111 #> Proof_Context.background_theory (fn thy => |
111 |> Context_Position.set_visible false |
112 thy |
112 |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound) |
113 |> Context_Position.set_visible_global false |
113 |> Proof_Context.background_theory (fn thy => |
114 |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound)))); |
114 thy |
|
115 |> Context_Position.set_visible_global false |
|
116 |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))); |
115 |
117 |
116 fun generic_try0 mode timeout_opt quad st = |
118 fun generic_try0 mode timeout_opt quad st = |
117 let |
119 let |
118 val st = Proof.map_contexts (silence_methods false) st; |
120 val st = Proof.map_contexts (silence_methods false) st; |
119 fun trd (_, _, t) = t; |
121 fun trd (_, _, t) = t; |