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