Coqide: try to properly send interrupts to coqtop on Win32

 We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having
 attached coqide to the console of the coqtop we want to interrupt.

 Two caveats:
 - This code isn't compatible with Windows < XP SP1.
 - It relies on the fact that coqide is now a true GUI app, without
   console by default. If for some reason the console of coqide is
   restored (for instance via mkwinapp -unset), strange behavior
   of the interrupt button is to be expected, at the very least all
   instances of coqtop will get Ctrl-C instead of a precise one.

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

7 files changed, 60 insertions, 16 deletions

diff --git a/CHANGES b/CHANGES
index 7cdaf0470..63adca842 100644
--- a/CHANGES
+++ b/CHANGES
@@ -106,8 +106,9 @@ Tools
 - Coq now searches directories specified in COQPATH and user-contribs before
   the standard library.
 - Coqide now runs coqtop as separated process, making it more robust:
-  coqtop subprocess can be interrupted (TODO check Win32), or even
-  killed and relaunched (cf button "Restart Coq", ex-"Go to Start").
+  coqtop subprocess can be interrupted, or even killed and relaunched
+  (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts,
+  the Windows version of coqide now requires Windows >= XP SP1.
 
 Changes from V8.2 to V8.3
 =========================
diff --git a/ide/coq.ml b/ide/coq.ml
index ef444292d..6e8190722 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -172,12 +172,13 @@ let spawn_coqtop sup_args =
 
 let respawn_coqtop coqtop = spawn_coqtop coqtop.sup_args
 
+let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
+let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
+
 let break_coqtop coqtop =
-  try Unix.kill coqtop.pid Sys.sigint
+  try !interrupter coqtop.pid
   with _ -> prerr_endline "Error while sending Ctrl-C"
 
-let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
-
 let kill_coqtop coqtop =
   let pid = coqtop.pid in
   begin
diff --git a/ide/coq.mli b/ide/coq.mli
index cef5d4246..04155ac40 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -41,6 +41,7 @@ val break_coqtop : coqtop -> unit
 (** In win32, we'll use a different kill function than Unix.kill *)
 
 val killer : (int -> unit) ref
+val interrupter : (int -> unit) ref
 
 (** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 915cd0603..6f0d81768 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -237,13 +237,9 @@ let force_reset_initial () =
   prerr_endline "Reset Initial";
   session_notebook#current_term.analyzed_view#force_reset_initial
 
-(* 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 break () =
+  prerr_endline "User break received";
+  Coq.break_coqtop !(session_notebook#current_term.toplvl)
 
 let do_if_not_computing text f x =
   let threaded_task () =
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 1987b97ac..9a9a0a0ed 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -41,12 +41,24 @@ let reroute_stdout_stderr () =
   Unix.dup2 out_descr Unix.stdout;
   Unix.dup2 out_descr Unix.stderr
 
-(* We also provide a specific kill function. *)
+(* We also provide specific kill and interrupt functions. *)
+
+(* Since [win32_interrupt] involves some hack about the process console,
+   only one should run at the same time, we simply skip execution of
+   [win32_interrupt] if another instance is already running *)
+
+let ctrl_c_mtx = Mutex.create ()
+
+let ctrl_c_protect f i =
+  if not (Mutex.try_lock ctrl_c_mtx) then ()
+  else try f i; Mutex.unlock ctrl_c_mtx with _ -> Mutex.unlock ctrl_c_mtx
 
 IFDEF Win32 THEN
 external win32_kill : int -> unit = "win32_kill"
+external win32_interrupt : int -> unit = "win32_interrupt"
 let () =
   Coq.killer := win32_kill;
+  Coq.interrupter := ctrl_c_protect win32_interrupt;
   set_win32_path ();
   reroute_stdout_stderr ()
 END
diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c
index 694f1c6a0..c09bf37de 100644
--- a/ide/ide_win32_stubs.c
+++ b/ide/ide_win32_stubs.c
@@ -1,3 +1,5 @@
+#define _WIN32_WINNT 0x0501  /* Cf below, we restrict to  */
+
 #include <caml/mlvalues.h>
 #include <caml/memory.h>
 #include <windows.h>
@@ -11,8 +13,37 @@
    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);
+CAMLprim value win32_kill(value pseudopid) {
+  CAMLparam1(pseudopid);
+  TerminateProcess((HANDLE)(Long_val(pseudopid)), 0);
+  CAMLreturn(Val_unit);
+}
+
+
+/* Win32 emulation of a kill -2 (SIGINT) */
+
+/* This code rely of the fact that coqide is now without initial console.
+   Otherwise, no console creation in win32unix/createprocess.c, hence
+   the same console for coqide and all coqtop, and everybody will be
+   signaled at the same time by the code below. */
+
+/* Moreover, AttachConsole exists only since WinXP, and GetProcessId
+   since WinXP SP1. For avoiding the GetProcessId, we could adapt code
+   from win32unix/createprocess.c to make it return both the pid and the
+   handle. For avoiding the AttachConsole, I don't know, maybe having
+   an intermediate process between coqide and coqtop ? */
+
+CAMLprim value win32_interrupt(value pseudopid) {
+  CAMLparam1(pseudopid);
+  HANDLE h;
+  DWORD pid;
+  FreeConsole(); /* Normally unnecessary, just to be sure... */
+  h = (HANDLE)(Long_val(pseudopid));
+  pid = GetProcessId(h);
+  AttachConsole(pid);
+  /* We want to survive the Ctrl-C that will also concerns us */
+  SetConsoleCtrlHandler(NULL,TRUE); /* NULL + TRUE means ignore */
+  GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); /* signal our co-console */
+  FreeConsole();
   CAMLreturn(Val_unit);
 }
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 928407058..42060c834 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -401,6 +401,8 @@ let extra_rules () = begin
     which moreover contains the Coq icon. If necessary, the mkwinapp
     tool can be used later to restore or suppress the console of Coqide. *)
 
+  if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico];
+
   if w32 then flag ["link"; "ocaml"; "program"; "ide"]
     (S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]);