[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.

4 files changed, 26 insertions, 34 deletions

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 *)