From ce2ce8f2c302e538514ecb48b0a8c41bdcb80124 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Apr 2018 09:36:51 +0200 Subject: 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. --- ide/ide_slave.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'ide') 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) -- cgit v1.2.3