Info: do not record info trace unless needed.

7 files changed, 44 insertions, 10 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 30af03cd9..4df5ab507 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -260,6 +260,11 @@ struct
   let current : P.e t = (); fun s ->
     { iolist = fun nil cons -> cons (s.rstate, s) nil }
 
+  let local (type a) (e:P.e) (m:a t) : a t = (); fun s ->
+    let m = m { s with rstate = e } in
+    { iolist = fun nil cons ->
+      m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) }
+
   let put (w : P.w) : unit t = (); fun s ->
     { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil }
 
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index 8006873ad..a36b017fb 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -137,6 +137,7 @@ module Logical (P:Param) : sig
   val modify : (P.s -> P.s) -> unit t
   val put : P.w -> unit t
   val current : P.e t
+  val local : P.e -> 'a t -> 'a t
   val update : (P.u -> P.u) -> unit t
 
   val zero : exn -> 'a t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c5eb03d5f..09d94a9ce 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -92,6 +92,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
       | Some etac -> Proofview.tclTHEN tac etac in
+    let tac = match info_lvl with
+      | None -> tac
+      | Some _ -> Proofview.Trace.record_info_trace tac
+    in
     let tac = match gi with
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ba61bf7a5..0a03965f1 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -210,7 +210,7 @@ type +'a tactic = 'a Proof.t
 (** Applies a tactic to the current proofview. *)
 let apply env t sp =
   let (next_r,(next_state,_),status,info) =
-    Logic_monad.NonLogical.run (Proof.run t () (sp,env))
+    Logic_monad.NonLogical.run (Proof.run t false (sp,env))
   in
   next_r,next_state,status,Trace.to_tree info
 
@@ -713,11 +713,12 @@ let tclTIMEOUT n t =
      already been computed. *)
   let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
   Proof.get >>= fun initial ->
+  Proof.current >>= fun envvar ->
   Proof.lift begin
     Logic_monad.NonLogical.catch
       begin
         let open Logic_monad.NonLogical in
-        timeout n (Proof.run t () initial) >>= fun r ->
+        timeout n (Proof.run t envvar initial) >>= fun r ->
         return (Util.Inl r)
       end
       begin let open Logic_monad.NonLogical in function
@@ -990,6 +991,8 @@ end
 
 module Trace = struct
 
+  let record_info_trace = InfoL.record_trace
+
   let log m = InfoL.leaf (Info.Msg m)
   let name_tactic m t = InfoL.tag (Info.Tactic m) t
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 52b9d3c11..29828bbbe 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -483,6 +483,10 @@ end
 
 module Trace : sig
 
+  (** [record_info_trace t] behaves like [t] except the [info] trace
+      is stored. *)
+  val record_info_trace : 'a tactic -> 'a tactic
+
   val log : Proofview_monad.lazy_msg -> unit tactic
   val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
 
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index 8f494c309..d1b255cc6 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
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index ef20415ce..8a2f95014 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -81,7 +81,8 @@ module P : sig
   val wunit : w
   val wprod : w -> w -> w
 
-  type e = unit
+  (** Recording info trace (true) or not. *)
+  type e = bool
 
   type u = Info.state
 
@@ -130,6 +131,9 @@ module Giveup : Writer with type t = Evar.t list
 
 (** Lens and utilies pertaining to the info trace *)
 module InfoL : sig
+  (** [record_trace t] behaves like [t] and compute its [info] trace. *)
+  val record_trace : 'a Logical.t -> 'a Logical.t
+
   val update : (Info.state -> Info.state) -> unit Logical.t
   val opn : Info.tag -> unit Logical.t
   val close : unit Logical.t