diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-15 19:47:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-15 19:48:53 +0100 |
| commit | e5b40d615d0ed9819f6ac8345ed924d8a501172e (patch) | |
| tree | d6d498ac9edeb97fe96fd6f06015b10ee5c871a1 | |
| parent | 45e43916a7ce756b617b7ba3f8062f7956872fb3 (diff) | |
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.
| -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 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 diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bd98fe16e..2e6a361c6 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 |