diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 5 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 1 |
2 files changed, 5 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 58f5eda62e..850b41e596 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 diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bd98fe16e3..2e6a361c66 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -361,6 +361,7 @@ let init = 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in Stm.set_compilation_hints file; + Stm.finish (); initial_id end |