diff options
| -rw-r--r-- | stm/stm.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 51 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 5 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 2 |
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 *) |