Ide: experimentally allow coqide to interrupt or kill coqtop

 - We now use create_process instead of open_process, and stores
   the answered pid.
 - The "Stop" button now sends a Sigint signal to this coqtop pid.
 - The "Goto Start" button now works even if a computation is ongoing,
   a new process is spawned and the previous one is killed -9, and
   then a waitpid is done to avoid having zombies around.

 Note that currently a vm_compute won't be stopped by a "Stop",
 but only by a "Goto Start". This can be quite confusing. How to
 properly document that "Goto Start" has the side effect of being
 a kill ? Maybe we could check someday if the Ctrl-C has been
 successful, and kill -9 if not ? Or maybe make coqide aware
 of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C
 in this case ?

 TODO:
  - for the moment a forced "Goto Start" displays an unfriendly anomaly
  - check if all this works under Windows (probably but not sure).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 0 deletions

diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index a4c4b1d9f..ff8dbb2d6 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -582,6 +582,7 @@ let make_cases s : string list list call =
 (* End of wrappers *)
 
 let loop () =
+  Sys.catch_break true;
   try
     while true do
       let q = (Marshal.from_channel: in_channel -> 'a call) stdin in