diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 18:29:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | 178672504f1c92b162c2575b14034cc7b698b6a4 (patch) | |
| tree | cb2fe74b45291b6b62020c0cf3a7fdebac46d15f /stm | |
| parent | b42b7073e47f03b6e907ffe902c72c72d82dbada (diff) | |
[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.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 7 insertions, 1 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 -> |