From e5b40d615d0ed9819f6ac8345ed924d8a501172e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 19:47:49 +0100 Subject: CoqIDE is more resilient to initialization errors. We force the STM to finish after the initialization request so as to raise exceptions that may have been generated by the initialization process. Likewise, we simply die when the initialization request fails in CoqIDE instead of just printing an error message. This is the fix for the underlying issue of bug #4591, but it does not solve the bug yet. --- ide/coqOps.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'ide/coqOps.ml') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 58f5eda62..850b41e59 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -864,7 +864,10 @@ object(self) method initialize = let get_initial_state = let next = function - | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return () + | Fail (_, _, message) -> + let message = "Couldn't initialize coqtop\n\n" ^ message in + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in + ignore (popup#run ()); exit 1 | Good id -> initial_state <- id; Coq.return () in Coq.bind (Coq.init (get_filename ())) next in Coq.seq get_initial_state Coq.PrintOpt.enforce -- cgit v1.2.3