diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 67 |
1 files changed, 36 insertions, 31 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7f2985aca..13b6eafc2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2148,23 +2148,42 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -let with_fail b f = - if not b then f () +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +(* Unfortunately we cannot cache here due to some bits in the STM not + being fully pure. *) +let freeze_interp_state marshallable = + { system = States.freeze ~marshallable; + proof = Proof_global.freeze ~marshallable; + shallow = marshallable = `Shallow } + +let unfreeze_interp_state { system; proof } = + States.unfreeze system; + Proof_global.unfreeze proof + +(* 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. * Note that error has to be printed in the right state, hence * within the purified function *) - Future.purify - (fun v -> - try f v; 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)))) - () + try 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 *) + unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2175,7 +2194,7 @@ let with_fail b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof (loc,c) = +let interp ?(verbosely=true) ?proof st (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function @@ -2188,7 +2207,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") | VernacLocal _ -> user_err Pp.(str "Locality specified twice") | VernacFail v -> - with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) + with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v @@ -2228,21 +2247,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -let freeze_interp_state marshallable = - { system = States.freeze ~marshallable; - proof = Proof_global.freeze ~marshallable; - shallow = (marshallable = `Shallow) } - -let unfreeze_interp_state { system; proof } = - States.unfreeze system; Proof_global.unfreeze proof - -let _dummy_interp_state = { system = Obj.magic 0; proof = Obj.magic 0; shallow = false } - let interp ?verbosely ?proof st cmd = - interp ?verbosely ?proof cmd; st + unfreeze_interp_state st; + interp ?verbosely ?proof st cmd; + freeze_interp_state `No |