diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 08:15:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 08:15:29 +0000 |
| commit | f418ecb6a2915a8b8b9fd5598ced5376cbcb75bc (patch) | |
| tree | b723d3010efabc8483d4652527f7634324618073 /library/states.ml | |
| parent | 43ee19f32c3ac89c7312b46f13ebdc50b6896b3b (diff) | |
Fixing bugs #2347 (part 2) and #2388: error message printing was done
too late, in a global environment which was no longer the correct one,
leading to the failure of error printing (hence an anomaly) in case
the command modified the state in several steps.
Now, errors raised by vernac commands are processed in the same
(intermediate) state they were raised from, just before rolling back
to the original state.
that modify the state in several
Now, errors raised by vernac commands that modify the state in several
steps (say S1, S2, ..., Sn) are processed in the state they were
produced in (S1, S2, ... Sn-1),
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/states.ml')
| -rw-r--r-- | library/states.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/states.ml b/library/states.ml index b7c66abf5..4619b3b53 100644 --- a/library/states.ml +++ b/library/states.ml @@ -28,12 +28,12 @@ let (extern_state,intern_state) = (* Rollback. *) -let with_heavy_rollback f x = +let with_heavy_rollback f h x = let st = freeze () in try f x with reraise -> - (unfreeze st; raise reraise) + let e = h reraise in (unfreeze st; raise e) let with_state_protection f x = let st = freeze () in |