diff options
| author | Emilio Jesus Gallego Arias | 2017-12-01 20:29:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-04 12:21:38 +0100 |
| commit | 195a652e38bcb6f58c156495492999ea8ee4e64e (patch) | |
| tree | 19788da699483c51d3560feb435fbec880d85911 | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
[vernac] Couple of tweaks missing from previous PRs.
In particular we must invalidate the state cache in the case of an
exception.
| -rw-r--r-- | vernac/vernacentries.ml | 9 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 28 |
2 files changed, 27 insertions, 10 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f8ec05fdbf..63768d9b88 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2268,5 +2268,10 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = comments on the PR *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; - interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + try + interp ?verbosely ?proof ~st cmd; + Vernacstate.freeze_interp_state `No + with exn -> + let exn = CErrors.push exn in + Vernacstate.invalidate_cache (); + iraise exn diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 4a1ae14e3c..4980333b5d 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -12,18 +12,30 @@ type t = { shallow : bool (* is the state trimmed down (libstack) *) } -let s_cache = ref (States.freeze ~marshallable:`No) -let s_proof = ref (Proof_global.freeze ~marshallable:`No) +let s_cache = ref None +let s_proof = ref None let invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 + s_cache := None; + s_proof := None + +let update_cache rf v = + rf := Some v; v + +let do_if_not_cached rf f v = + match !rf with + | None -> + rf := Some v; f v + | Some vc when vc != v -> + rf := Some v; f v + | Some _ -> + () let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); + { system = update_cache s_cache (States.freeze ~marshallable); + proof = update_cache s_proof (Proof_global.freeze ~marshallable); shallow = marshallable = `Shallow } let unfreeze_interp_state { system; proof } = - if (!s_cache != system) then (s_cache := system; States.unfreeze system); - if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) + do_if_not_cached s_cache States.unfreeze system; + do_if_not_cached s_proof Proof_global.unfreeze proof |