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

8 files changed, 70 insertions, 27 deletions

diff --git a/config/Makefile.template b/config/Makefile.template
index cd92fc446..c5d81c9d0 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -138,9 +138,9 @@ STRIP=STRIPCOMMAND
 
 # CoqIde (no/byte/opt)
 HASCOQIDE=COQIDEOPT
-IDEOPTFLAGS=MACIGEFLAGS
-IDEOPTDEPS=MACIGEFILE
-IDEOPTP4=MACIGEP4
+IDEOPTFLAGS=IDEARCHFLAGS
+IDEOPTDEPS=IDEARCHFILE
+IDEOPTP4=IDEARCHDEF
 
 # Defining REVISION
 CHECKEDOUT=CHECKEDOUTSOURCETREE
diff --git a/configure b/configure
index 4b6004f26..97f629c05 100755
--- a/configure
+++ b/configure
@@ -597,6 +597,10 @@ esac
 
 # lablgtk2 and CoqIDE
 
+IDEARCHFLAGS=
+IDEARCHFILE=
+IDEARCHDEF=
+
 # -byte-only should imply -coqide byte, unless the user decides otherwise
 
 if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then 
@@ -639,16 +643,17 @@ else
         echo "LablGtk2 found, native threads: native CoqIde will be available."
 	COQIDE=opt
         if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
-            then 
+        then
             cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
-            MACIGEFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
-            MACIGEFILE=ide/ide_mac_stubs.o
-            MACIGEP4=-DMacInt
-            else
-            MACIGEFLAGS=""
-            MACIGEFILE=""
-            MACIGEP4=""
-            fi
+	    IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
+	    IDEARCHFILE=ide/ide_mac_stubs.o
+	    IDEARCHDEF=-DMacInt
+	elif [ "$ARCH" = "win32" ];
+        then
+	    IDEARCHFLAGS=
+	    IDEARCHFILE=ide/ide_win32_stubs.o
+	    IDEARCHDEF=-DWin32
+	fi
     fi
 fi
 
@@ -876,7 +881,7 @@ fi
 if test "$COQIDE" != "no"; then
 echo "  Lablgtk2 library in               : $LABLGTKLIB"
 fi
-if test "$MACIGEFILE" != ""; then
+if test "$IDEARCHDEF" = "-DMacInt"; then
 echo "  Mac OS integration is on"
 fi
 if test "$with_doc" = "all"; then
@@ -1108,9 +1113,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|RANLIBEXEC|$ranlib_exec|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
     -e "s|COQIDEOPT|$COQIDE|" \
-    -e "s|MACIGEFLAGS|$MACIGEFLAGS|" \
-    -e "s|MACIGEFILE|$MACIGEFILE|" \
-    -e "s|MACIGEP4|$MACIGEP4|" \
+    -e "s|IDEARCHFLAGS|$IDEARCHFLAGS|" \
+    -e "s|IDEARCHFILE|$IDEARCHFILE|" \
+    -e "s|IDEARCHDEF|$IDEARCHDEF|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
     -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
diff --git a/ide/coq.ml b/ide/coq.ml
index d595fbc91..1d67e8ee7 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 58bedca1b..a9c41de62 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 65409c2de..63754fd51 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 d5888ff93..ceeaa199d 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 000000000..694f1c6a0
--- /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);
+}
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 97f91666e..928407058 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -288,6 +288,11 @@ let extra_rules () = begin
   flag_and_dep ["p4mod"; "use_compat5"] (P "tools/compat5.cmo");
   flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo");
 
+  if w32 then begin
+    flag ["p4mod"] (A "-DWin32");
+    dep ["ocaml"; "link"; "ide"] ["ide/ide_win32_stubs.o"];
+  end;
+
   if not use_camlp5 then begin
   let mlp_cmo s =
     let src=s^".mlp" and dst=s^".cmo" in