diff options
| author | gareuselesinge | 2013-10-22 14:31:44 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-22 14:31:44 +0000 |
| commit | b16c1a41dc9e4a00abb734dc820fff396c338634 (patch) | |
| tree | 09f1139b8ce7ed0c366e83ec092ec90abc98b608 | |
| parent | cd3f043404181514ff44357058e7bf705c865504 (diff) | |
STM: do not enrich exceptions more than once
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16908 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/stm.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index fdd24f7e48..f63cd9e4e5 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -533,10 +533,13 @@ end = struct (* {{{ *) let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) let exn_on id ?valid e = - let loc = Option.default Loc.ghost (Loc.get_loc e) in - let msg = string_of_ppcmds (print e) in - Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); - Stateid.add e ?valid id + match Stateid.get e with + | Some _ -> e + | None -> + let loc = Option.default Loc.ghost (Loc.get_loc e) in + let msg = string_of_ppcmds (print e) in + Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); + Stateid.add e ?valid id let define ?(redefine=false) ?(cache=`No) f id = let str_id = Stateid.to_string id in |