diff options
| author | Arnaud Spiwack | 2014-10-30 14:50:59 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | bfa71dfcf722dfc0e1f1cd616945cc3e1da9d5ba (patch) | |
| tree | 9f0e2d59404a8cf63f44b7dc7d31eb2a10286003 /proofs/proofview_monad.ml | |
| parent | d47c178be6e5dc52fedbb312fc51673623608994 (diff) | |
Info: do not record info trace unless needed.
Diffstat (limited to 'proofs/proofview_monad.ml')
| -rw-r--r-- | proofs/proofview_monad.ml | 27 |
1 files changed, 20 insertions, 7 deletions
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml index 8f494c3098..d1b255cc66 100644 --- a/proofs/proofview_monad.ml +++ b/proofs/proofview_monad.ml @@ -167,8 +167,8 @@ module P = struct type s = proofview * Environ.env - type e = unit - (* spiwack: nothing read-only anymore but it's free so I'll leave a place holder. *) + (** Recording info trace (true) or not. *) + type e = bool (** Status (safe/unsafe) * shelved goals * given up *) type w = bool * Evar.t list * Evar.t list @@ -243,15 +243,28 @@ end (** Lens and utilies pertaining to the info trace *) module InfoL = struct - let update = Logical.update + let recording = Logical.current + let if_recording t = + let open Logical in + recording >>= fun r -> + if r then t else return () + + let record_trace t = Logical.local true t + + let raw_update = Logical.update + let update f = if_recording (raw_update f) let opn a = update (Trace.opn a) let close = update Trace.close let leaf a = update (Trace.leaf a) let tag a t = let open Logical in - opn a >> - t >>= fun a -> - close >> - return a + recording >>= fun r -> + if r then begin + raw_update (Trace.opn a) >> + t >>= fun a -> + raw_update Trace.close >> + return a + end else + t end |