1\DOC trace 2 3\TYPE {trace : string * int -> ('a -> 'b) -> 'a -> 'b} 4 5\SYNOPSIS 6Invoke a function with a specified level of tracing. 7 8\KEYWORDS 9Tracing. 10 11\DESCRIBE 12The {trace} function is used to set the value of a tracing variable 13for the duration of one top-level function call. 14 15A call to {trace (nm,i) f x} attempts to set the tracing variable 16associated with the string {nm} to value {i}. Then it evaluates 17{f x} and returns the resulting value after restoring the 18trace level of {nm}. 19 20\FAILURE 21Fails if the name given is not associated with a registered tracing 22variable. Also fails if the function invocation fails. 23 24\EXAMPLE 25{ 26- load "mesonLib"; 27 28- trace ("meson",2) prove 29 (concl SKOLEM_THM,mesonLib.MESON_TAC []); 30 310 inferences so far. Searching with maximum size 0. 320 inferences so far. Searching with maximum size 1. 33Internal goal solved with 2 MESON inferences. 340 inferences so far. Searching with maximum size 0. 350 inferences so far. Searching with maximum size 1. 36Internal goal solved with 2 MESON inferences. 370 inferences so far. Searching with maximum size 0. 380 inferences so far. Searching with maximum size 1. 39Internal goal solved with 2 MESON inferences. 400 inferences so far. Searching with maximum size 0. 410 inferences so far. Searching with maximum size 1. 42Internal goal solved with 2 MESON inferences. 43 solved with 2 MESON inferences. 44 45> val it = |- !P. (!x. ?y. P x y) = ?f. !x. P x (f x) : thm 46 47- traces(); 48 49> val it = 50 [{default = 1, name = "meson", trace_level = 1}, 51 {default = 10, name = "Subgoal number", trace_level = 10}, 52 {default = 0, name = "Rewrite", trace_level = 0}, 53 {default = 0, name = "Ho_Rewrite", trace_level = 0}] 54} 55 56 57\SEEALSO 58Feedback, Feedback.register_trace, Feedback.reset_trace, Feedback.reset_traces, Feedback.set_trace, Feedback.traces, Lib.with_flag. 59\ENDDOC 60