Coqide: a special kill function for win32

 This is implemented as a C external launching the TerminateProcess
 of the Win32 API. This should be considered as quite experimental
 (cf. the way we handle pid in the comment of ide_win32_stubs.c).

 I don't know how to emulate an interrupt (Ctrl-C), for now the two
 button "Restart" and "Interrupt" have the same semantics on win32
 (kill the subprocess and start at top).

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

5 files changed, 44 insertions, 11 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index d595fbc91e..1d67e8ee70 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -167,9 +167,11 @@ let break_coqtop coqtop =
   try Unix.kill coqtop.pid Sys.sigint
   with _ -> prerr_endline "Error while sending Ctrl-C"
 
+let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
+
 let blocking_kill pid =
   begin
-    try Unix.kill pid Sys.sigkill;
+    try !killer pid
     with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
   end;
   try
diff --git a/ide/coq.mli b/ide/coq.mli
index 58bedca1b9..a9c41de626 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -40,6 +40,10 @@ val reset_coqtop : coqtop -> coqtop
 
 val process_exn : exn -> Ide_intf.location * string
 
+(** In win32, we'll use a different kill function than Unix.kill *)
+
+val killer : (int -> unit) ref
+
 (** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
 val interp : coqtop -> bool -> string -> unit Ide_intf.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 65409c2de4..63754fd510 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -227,14 +227,18 @@ let coq_computing = Mutex.create ()
 (* To prevent Coq from interrupting during undoing...*)
 let coq_may_stop = Mutex.create ()
 
-let break () =
-  prerr_endline "User break received";
-  Coq.break_coqtop !(session_notebook#current_term.toplvl)
-
 let force_reset_initial () =
   prerr_endline "Reset Initial";
   session_notebook#current_term.analyzed_view#reset_initial true
 
+(* How could we interrupt nicely coqtop in win32 ?
+   For the moment, we simply kill it brutally *)
+let break =
+  if Sys.os_type = "Win32" then force_reset_initial
+  else fun () ->
+    prerr_endline "User break received";
+    Coq.break_coqtop !(session_notebook#current_term.toplvl)
+
 let do_if_not_computing text f x =
   let threaded_task () =
     if Mutex.try_lock coq_computing then
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index d5888ff938..ceeaa199d2 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -19,15 +19,20 @@ let initmac () = IFDEF MacInt THEN gtk_mac_init Coqide.do_load Coqide.forbid_qui
 let macready () = IFDEF MacInt THEN gtk_mac_ready () ELSE ()  END
 
 (* On win32, we add the directory of coqide to the PATH at launch-time
-   (this used to be done in a .bat script). *)
+   (this used to be done in a .bat script).
+   We also provide a specific kill function.
+*)
 
-let winpath () =
-  if Coq_config.arch = "win32" then
-    Unix.putenv "PATH" (Filename.dirname Sys.executable_name ^ ";" ^
-			  (try Sys.getenv "PATH" with _ -> ""))
+IFDEF Win32 THEN
+external win32_kill : int -> unit = "win32_kill"
+let () =
+  Unix.putenv "PATH"
+    (Filename.dirname Sys.executable_name ^ ";" ^
+      (try Sys.getenv "PATH" with _ -> ""));
+  Coq.killer := win32_kill
+END
 
 let () =
-  winpath ();
   let argl = Array.to_list Sys.argv in
   let argl = Coqide.set_coqtop_path argl in
   let files = Coqide.process_argv argl in
diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c
new file mode 100644
index 0000000000..694f1c6a02
--- /dev/null
+++ b/ide/ide_win32_stubs.c
@@ -0,0 +1,18 @@
+#include <caml/mlvalues.h>
+#include <caml/memory.h>
+#include <windows.h>
+
+/* Win32 emulation of kill -9 */
+
+/* The pid returned by Unix.create_process is actually a pseudo-pid,
+   made via a cast of the obtained HANDLE, (cf. win32unix/createprocess.c
+   in the sources of ocaml). Since we're still in the caller process,
+   we simply cast back to get an handle...
+   The 0 is the exit code we want for the terminated process.
+*/
+
+CAMLprim value win32_kill(value pid) {
+  CAMLparam1(pid);
+  TerminateProcess((HANDLE)(Long_val(pid)), 0);
+  CAMLreturn(Val_unit);
+}