diff options
-rw-r--r-- | config/Makefile.template | 6 | ||||
-rwxr-xr-x | configure | 31 | ||||
-rw-r--r-- | ide/coq.ml | 4 | ||||
-rw-r--r-- | ide/coq.mli | 4 | ||||
-rw-r--r-- | ide/coqide.ml | 12 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 17 | ||||
-rw-r--r-- | ide/ide_win32_stubs.c | 18 | ||||
-rw-r--r-- | myocamlbuild.ml | 5 |
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 @@ -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 |