[vernac] Refactor common parts of interp_{,delayed}

This should fix some bugs w.r.t. management of state introduced in

3 files changed, 35 insertions, 41 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 17cef26997..7f0632bd7c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1056,7 +1056,7 @@ end (* }}} *)
 (* Wrapper for the proof-closing special path for Qed *)
 let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
   set_id_for_feedback ?route dummy_doc id;
-  Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc ~control pending
+  Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending)
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 74438f3c16..819d1acfb5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2249,11 +2249,11 @@ let locate_if_not_already ?loc (e, info) =
   | None   -> (e, Option.cata (Loc.add_loc info) info loc)
   | Some l -> (e, info)
 
-let mk_time_header ~vernac =
+let mk_time_header =
+  (* Drop the time header to print the command, we should indeed use a
+     different mechanism to `-time` commands than the current hack of
+     adding a time control to the AST. *)
   let pr_time_header vernac =
-    (* Drop the time header to print the command, we should indeed use a
-       different mechanism to `-time` commands than the current hack of
-       adding a time control to the AST. *)
     let vernac = match vernac with
       | { v = { control = ControlTime _ :: control; attrs; expr }; loc } ->
         CAst.make ?loc { control; attrs; expr }
@@ -2261,7 +2261,7 @@ let mk_time_header ~vernac =
     in
     Topfmt.pr_cmd_header vernac
   in
-  Lazy.from_fun (fun () -> pr_time_header vernac)
+  fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac)
 
 let interp_control_flag ~time_header (f : control_flag) ~st
     (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
@@ -2702,7 +2702,7 @@ and vernac_load ~verbosely fname =
   ()
 
 and interp_control ~st ({ v = cmd } as vernac) =
-  let time_header = mk_time_header ~vernac in
+  let time_header = mk_time_header vernac in
   List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
     cmd.control
     (fun ~st ->
@@ -2712,6 +2712,25 @@ and interp_control ~st ({ v = cmd } as vernac) =
        else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack)
     ~st
 
+(* Interpreting a possibly delayed proof *)
+let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
+  let stack = st.Vernacstate.lemmas in
+  let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
+  let () = match pe with
+    | Admitted ->
+      save_lemma_admitted_delayed ~proof ~info
+    | Proved (_,idopt) ->
+      save_lemma_proved_delayed ~proof ~info ~idopt in
+  stack
+
+let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } =
+  let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
+  List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+    control
+    (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
+    ~st
+
+(* General interp with management of state *)
 let () =
   declare_int_option
     { optdepr  = false;
@@ -2721,11 +2740,11 @@ let () =
       optwrite = ((:=) default_timeout) }
 
 (* Be careful with the cache here in case of an exception. *)
-let interp ?(verbosely=true) ~st cmd =
+let interp_gen ~verbosely ~st ~interp_fn cmd =
   Vernacstate.unfreeze_interp_state st;
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
-      let ontop = v_mod (interp_control ~st) cmd in
+      let ontop = v_mod (interp_fn ~st) cmd in
       Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
@@ -2735,34 +2754,10 @@ let interp ?(verbosely=true) ~st cmd =
     Vernacstate.invalidate_cache ();
     iraise exn
 
-(* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
-  let stack = st.Vernacstate.lemmas in
-  let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
-  let () = match pe with
-    | Admitted ->
-      save_lemma_admitted_delayed ~proof ~info
-    | Proved (_,idopt) ->
-      save_lemma_proved_delayed ~proof ~info ~idopt in
-  stack
-
-let interp_qed_delayed_control ~proof ~info ~st ?loc ~control pe : Vernacstate.t =
-  let vernac = CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe } in
-  let time_header = mk_time_header ~vernac in
-  let stack =
-    List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
-      control
-      (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
-      ~st
-  in
-  Vernacstate.Proof_global.set stack [@ocaml.warning "-3"];
-  Vernacstate.freeze_interp_state ~marshallable:false
+(* Regular interp *)
+let interp ?(verbosely=true) ~st cmd =
+  interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
 
-let interp_qed_delayed_proof ~proof ~info ~st ?loc ~control pe : Vernacstate.t =
-  try
-    interp_qed_delayed_control ~proof ~info ~st ?loc ~control pe
-  with exn ->
-    let exn = CErrors.push exn in
-    let exn = locate_if_not_already ?loc exn in
-    Vernacstate.invalidate_cache ();
-    iraise exn
+let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t =
+  interp_gen ~verbosely:false ~st
+    ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index ad5a849fed..e65f9d3cfe 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -17,9 +17,8 @@ val interp_qed_delayed_proof
   :  proof:Proof_global.proof_object
   -> info:Lemmas.Info.t
   -> st:Vernacstate.t
-  -> ?loc:Loc.t
   -> control:Vernacexpr.control_flag list
-  -> Vernacexpr.proof_end
+  -> Vernacexpr.proof_end CAst.t
   -> Vernacstate.t
 
 (** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)