diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-18 15:16:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-18 15:19:00 +0100 |
| commit | 16939df43a089ac30fec0fcf30a2f648d007cb60 (patch) | |
| tree | 98046b9b2f7671d27ac8e69702afa6b0e2a457ef /ide | |
| parent | b4b98349d03c31227d0d86a6e3acda8c3cd5212c (diff) | |
| parent | 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 (diff) | |
Merge branch 'v8.5'
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 6200f1490..aa1a75db6 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -869,7 +869,10 @@ object(self) method initialize = let get_initial_state = let next = function - | Fail _ -> messages#set (Richpp.richpp_of_string "Couln't initialize Coq"); Coq.return () + | Fail (_, _, message) -> + let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print 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 12ef0e075..9a3e85e47 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -371,6 +371,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 |