From 041c09d0f59b420285723d000e4ea08fb2d3fb2d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 2 Mar 2019 20:57:45 +0100
Subject: [Fail] Simplify `Fail` implementation.

We can now implement `Fail` in a direct style.
---
 vernac/vernacentries.ml | 39 +++++++++++++++------------------------
 1 file changed, 15 insertions(+), 24 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ac47a6a8f3..fd6ca210b0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2291,36 +2291,27 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
     f x
 
 (* Fail *)
-exception HasNotFailed
-exception HasFailed of Pp.t
-
 let test_mode = ref false
 
-(* XXX STATE: this type hints that restoring the state should be the
-   caller's responsibility *)
+(* XXX STATE: the type hints that restoring the state should be the
+   caller's responsibility, see how we restore it in the two
+   branches. *)
 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 let _ = f () in raise HasNotFailed
-    with
-    | HasNotFailed as e -> raise e
-    | e when CErrors.noncritical e || e = Timeout ->
-      let e = CErrors.push e in
-      raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error e)))
-  with e when CErrors.noncritical e ->
-    (* Restore the previous state XXX Careful here with the cache! *)
+    let _ = f () in
+    Vernacstate.invalidate_cache ();
+    Vernacstate.unfreeze_interp_state st;
+    user_err ~hdr:"Fail" (str "The command has not failed!")
+  with
+  (* Fail Timeout is a common pattern so we need to support it. *)
+  | e when CErrors.noncritical e || e = Timeout ->
+    (* The error has to be printed in the failing state *)
+    let msg = CErrors.(iprint ExplainErr.(process_vernac_interp_error (push e))) in
+    (* Restore the previous state; 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
+    if not !Flags.quiet || !test_mode
+    then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg)
 
 let locate_if_not_already ?loc (e, info) =
   match Loc.get_loc info with
-- 
cgit v1.2.3


From 8a6a3b4f6cbdaf2047ab30b7eaf451c166a874bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 16 Jun 2019 17:31:07 +0200
Subject: [Fail] Tweaks to implementation.

We handle state restoration outside the main fail logic, as in the
future it could be that vernac execution is fully functional so we
could get rid of the second part.
---
 vernac/vernacentries.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fd6ca210b0..a3d873cd40 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2293,23 +2293,26 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
 (* Fail *)
 let test_mode = ref false
 
-(* XXX STATE: the type hints that restoring the state should be the
-   caller's responsibility, see how we restore it in the two
-   branches. *)
-let with_fail ~st f =
+(* Restoring the state is the caller's responsibility *)
+let with_fail f : (Pp.t, unit) result =
   try
     let _ = f () in
-    Vernacstate.invalidate_cache ();
-    Vernacstate.unfreeze_interp_state st;
-    user_err ~hdr:"Fail" (str "The command has not failed!")
+    Error ()
   with
   (* Fail Timeout is a common pattern so we need to support it. *)
   | e when CErrors.noncritical e || e = Timeout ->
     (* The error has to be printed in the failing state *)
-    let msg = CErrors.(iprint ExplainErr.(process_vernac_interp_error (push e))) in
-    (* Restore the previous state; careful here with the cache! *)
-    Vernacstate.invalidate_cache ();
-    Vernacstate.unfreeze_interp_state st;
+    Ok CErrors.(iprint ExplainErr.(process_vernac_interp_error (push e)))
+
+(* We restore the state always *)
+let with_fail ~st f =
+  let res = with_fail f in
+  Vernacstate.invalidate_cache ();
+  Vernacstate.unfreeze_interp_state st;
+  match res with
+  | Error () ->
+    user_err ~hdr:"Fail" (str "The command has not failed!")
+  | Ok msg ->
     if not !Flags.quiet || !test_mode
     then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg)
 
-- 
cgit v1.2.3