[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.

We try to do a bit of cleanup for the `with_fail` function, this still
is delicate code.

5 files changed, 33 insertions, 35 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index c11f8d86e6..cc0de0e9df 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2064,6 +2064,12 @@ end = struct (* {{{ *)
 
   module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
 
+  let stm_fail ~st fail f =
+    if fail then
+      Vernacentries.with_fail ~st f
+    else
+      f ()
+
   let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen } : unit
   =
@@ -2075,7 +2081,7 @@ end = struct (* {{{ *)
         | e -> e, time, batch, fail in
       find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
-    Vernacstate.Proof_global.with_fail ~st (fun () ->
+    stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Vernacstate.Proof_global.with_current_proof (fun _ p ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5d73d2e401..91965e56b1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2589,41 +2589,38 @@ let test_mode = ref false
 
 (* XXX STATE: this type hints that restoring the state should be the
    caller's responsibility *)
-let with_fail ~st b f =
-  if not b
-  then f ()
-  else begin try
-      (* If the command actually works, ignore its effects on the state.
+let with_fail ~st f =
+  try
+    (* If the command actually works, ignore its effects on the state.
        * Note that error has to be printed in the right state, hence
        * within the purified function *)
-      try ignore (f ()); raise HasNotFailed
-      with
-      | HasNotFailed as e -> raise e
-      | e ->
-        let e = CErrors.push e in
-        raise (HasFailed (CErrors.iprint
-                            (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
-    with e when CErrors.noncritical e ->
-      (* Restore the previous state XXX Careful here with the cache! *)
-      Vernacstate.invalidate_cache ();
-      Vernacstate.unfreeze_interp_state st;
-      let (e, _) = CErrors.push e in
-      match e with
-      | HasNotFailed ->
-          user_err ~hdr:"Fail" (str "The command has not failed!")
-      | HasFailed msg ->
-          if not !Flags.quiet || !test_mode then Feedback.msg_info
-            (str "The command has indeed failed with message:" ++ fnl () ++ msg);
-          st.Vernacstate.proof
-      | _ -> assert false
-  end
+    try let _ = f () in raise HasNotFailed
+    with
+    | HasNotFailed as e -> raise e
+    | e ->
+      let e = CErrors.push e in
+      raise (HasFailed (CErrors.iprint
+                          (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
+  with e when CErrors.noncritical e ->
+    (* Restore the previous state XXX Careful here with the cache! *)
+    Vernacstate.invalidate_cache ();
+    Vernacstate.unfreeze_interp_state st;
+    let (e, _) = CErrors.push e in
+    match e with
+    | HasNotFailed ->
+      user_err ~hdr:"Fail" (str "The command has not failed!")
+    | HasFailed msg ->
+      if not !Flags.quiet || !test_mode then Feedback.msg_info
+          (str "The command has indeed failed with message:" ++ fnl () ++ msg)
+    | _ -> assert false
 
 let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} : Proof_global.t option =
   let rec control ~st = function
   | VernacExpr (atts, v) ->
     aux ~atts ~st v
   | VernacFail v ->
-    with_fail ~st true (fun () -> control ~st v)
+    with_fail ~st (fun () -> ignore(control ~st v));
+    st.Vernacstate.proof
   | VernacTimeout (n,v) ->
     current_timeout := Some n;
     control ~st v
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 2e6477995a..71cc29b6e1 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -33,9 +33,8 @@ val interp :
 
 val make_cases : string -> string list list
 
-(* XXX STATE: this type hints that restoring the state should be the
-   caller's responsibility *)
-val with_fail : st:Vernacstate.t -> bool -> (unit -> Proof_global.t option) -> Proof_global.t option
+(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)
+val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit
 
 val command_focus : unit Proof.focus_kind
 
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 01c7068f33..77f54361da 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -75,8 +75,6 @@ let make_shallow st =
 (* Compatibility module *)
 module Proof_global = struct
 
-  let with_fail ~st f = f ()
-
   let get () = !s_proof
   let set x = s_proof := x
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 42a87cfbd0..b79f97796f 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -36,8 +36,6 @@ val invalidate_cache : unit -> unit
 (* Compatibility module: Do Not Use *)
 module Proof_global : sig
 
-  val with_fail : st:t -> (unit -> unit) -> unit
-
   open Proof_global
 
   (* Low-level stuff *)