diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-28 10:09:12 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-28 10:09:12 +0000 |
commit | f5276a11a40f86d5ed8ff14bd03d6ea71e7dad33 (patch) | |
tree | 45ac7fcd7ae7a24ba861371586107df42056344d /ide | |
parent | eee95fec8763a6323f27b86a5ee115305d4f3d9d (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.ml | 7 | ||||
-rw-r--r-- | ide/coq.mli | 1 | ||||
-rw-r--r-- | ide/coqide.ml | 10 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 14 | ||||
-rw-r--r-- | ide/ide_win32_stubs.c | 37 |
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); } |