aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-04-12 09:36:51 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-04-12 09:36:51 +0200
commitce2ce8f2c302e538514ecb48b0a8c41bdcb80124 (patch)
tree293dbb546beecc2bb738d177b7fae99f2c272d84
parent8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff)
Attempt to fix the doubly encapsulated Ltac errors in coqide.
It seems that ExplainErr.process_vernac_interp_error is called twice in CoqIDE. First time in Stm.stm_vernac_interp (via Stm.call_process_error_once). Second time in the "handle_exn" method used by CoqIDE to handle exceptions coming from Coq (ide_slave.ml/xmlprotocol.ml). The proposed fix is to remove the call in CoqIDE, assuming that the process_vernac_interp_error call is done otherwise on all potential error paths.
-rw-r--r--ide/ide_slave.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 2e552b60b..5abd7803a 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -352,7 +352,6 @@ let about () = {
}
let handle_exn (e, info) =
- let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in
let dummy = Stateid.dummy in
let loc_of e = match Loc.get_loc e with
| Some loc -> Some (Loc.unloc loc)