aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml5
1 files changed, 4 insertions, 1 deletions
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