with_flag
Lib.with_flag : 'a ref * 'a -> ('b -> 'c) -> 'b -> 'c
Apply a function under a particular flag setting.
An invocation with_flag (r,v) f x sets the reference variable r to
the value v, then evaluates f x, then resets r to its original
value, and returns the value of f x.
Failure
Fails if f x fails. In that case, r is reset to its original value
before raising the exception from f x.
Example
> fun print_term_nl tm = (print_term tm; Feedback.HOL_INFO "\n");
val print_term_nl = fn: term -> unit
> with_flag (show_types, true) print_term_nl (concl T_DEF);
T ⇔ (λ(x :bool). x) = (λ(x :bool). x)
val it = (): unit
> print_term_nl (concl T_DEF);
T ⇔ (λx. x) = (λx. x)
val it = (): unit
See also
Feedback.traces,
Feedback.register_btrace,
Feedback.trace, Lib.time