aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-28 10:09:12 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-28 10:09:12 +0000
commitf5276a11a40f86d5ed8ff14bd03d6ea71e7dad33 (patch)
tree45ac7fcd7ae7a24ba861371586107df42056344d /ide
parenteee95fec8763a6323f27b86a5ee115305d4f3d9d (diff)
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
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml7
-rw-r--r--ide/coq.mli1
-rw-r--r--ide/coqide.ml10
-rw-r--r--ide/coqide_main.ml414
-rw-r--r--ide/ide_win32_stubs.c37
5 files changed, 55 insertions, 14 deletions
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);
}