aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml57
-rw-r--r--ide/coq.mli8
-rw-r--r--ide/coqide.ml27
-rw-r--r--ide/coqide.mli2
-rw-r--r--ide/coqide_main.ml42
-rw-r--r--toplevel/ide_blob.ml1
6 files changed, 51 insertions, 46 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 285133d48..89040aa5f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -26,19 +26,13 @@ open Ideutils
open Compat
type coqtop = {
+ mutable pid : int;
mutable cout : in_channel ;
mutable cin : out_channel ;
- sup_args : string ;
+ sup_args : string list;
mutable version : int ;
}
-let dummy_coqtop = {
- cout = stdin ;
- cin = stdout ;
- sup_args = "" ;
- version = 0 ;
-}
-
let prerr_endline s = if !debug then prerr_endline s else ()
let output = ref (Format.formatter_of_out_channel stdout)
@@ -109,7 +103,8 @@ exception Coqtop_output of string list
let check_connection args =
try
- let ic = Unix.open_process_in (coqtop_path () ^ " -batch "^args) in
+ let args = String.concat " " ("-batch"::args) in
+ let ic = Unix.open_process_in (coqtop_path () ^ " " ^ args) in
let lines = read_all_lines ic in
match (Unix.close_process_in ic) with
| Unix.WEXITED 0 -> prerr_endline "coqtop seems ok"
@@ -142,27 +137,42 @@ let toplvl_ctr_mtx = Mutex.create ()
let spawn_coqtop sup_args =
Mutex.lock toplvl_ctr_mtx;
- try
- let oc,ic = Unix.open_process (coqtop_path ()^" -ideslave "^sup_args) in
- set_binary_mode_out ic true;
- set_binary_mode_in oc true;
+ try
+ let (in_read,in_write) = Unix.pipe () in
+ let (out_read,out_write) = Unix.pipe () in
+ let prog = coqtop_path () in
+ let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
+ let pid = Unix.create_process prog args out_read in_write Unix.stderr in
+ assert (pid <> 0);
+ Unix.close out_read;
+ Unix.close in_write;
+ let ic = Unix.in_channel_of_descr in_read in
+ let oc = Unix.out_channel_of_descr out_write in
+ set_binary_mode_out oc true;
+ set_binary_mode_in ic true;
incr toplvl_ctr;
Mutex.unlock toplvl_ctr_mtx;
- { cin = ic; cout = oc ; sup_args = sup_args ; version = 0 }
+ { pid = pid; cin = oc; cout = ic ; sup_args = sup_args ; version = 0 }
with e ->
Mutex.unlock toplvl_ctr_mtx;
raise e
+let break_coqtop coqtop =
+ try Unix.kill coqtop.pid Sys.sigint
+ with _ -> prerr_endline "Error while sending Ctrl-C"
+
+let blocking_kill pid =
+ begin
+ try Unix.kill pid Sys.sigkill;
+ with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
+ end;
+ try
+ ignore (Unix.waitpid [] pid);
+ Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
+ with _ -> prerr_endline "Error while waiting for child"
+
let kill_coqtop coqtop =
- let ic = coqtop.cin in
- let oc = coqtop.cout in
- ignore (Thread.create
- (fun () ->
- try
- ignore (Unix.close_process (oc,ic));
- Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
- with _ -> prerr_endline "Process leak")
- ())
+ ignore (Thread.create blocking_kill coqtop.pid)
let coqtop_zombies =
(fun () ->
@@ -176,6 +186,7 @@ let reset_coqtop coqtop =
let ni = spawn_coqtop coqtop.sup_args in
coqtop.cin <- ni.cin;
coqtop.cout <- ni.cout;
+ coqtop.pid <- ni.pid
module PrintOpt =
struct
diff --git a/ide/coq.mli b/ide/coq.mli
index 6bc593477..c909a559f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -15,16 +15,16 @@ open Ide_blob
val short_version : unit -> string
val version : unit -> string
val filter_coq_opts : string list -> bool * string list
-val check_connection : string -> unit
+val check_connection : string list -> unit
type coqtop
-val dummy_coqtop : coqtop
-
-val spawn_coqtop : string -> coqtop
+val spawn_coqtop : string list -> coqtop
val kill_coqtop : coqtop -> unit
+val break_coqtop : coqtop -> unit
+
val coqtop_zombies : unit -> int
val reset_coqtop : coqtop -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5ebea7589..475b8f8a4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -217,20 +217,12 @@ let coq_computing = Mutex.create ()
let coq_may_stop = Mutex.create ()
let break () =
- prerr_endline "User break received:";
- if not (Mutex.try_lock coq_computing) then
- begin
- prerr_endline " trying to stop computation:";
- if Mutex.try_lock coq_may_stop then begin
- Util.interrupt := true;
- prerr_endline " interrupt flag set. Computation should stop soon...";
- Mutex.unlock coq_may_stop
- end else prerr_endline " interruption refused (may not stop now)";
- end
- else begin
- Mutex.unlock coq_computing;
- prerr_endline " ignored (not computing)"
- end
+ 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
let do_if_not_computing text f x =
let threaded_task () =
@@ -242,7 +234,8 @@ let do_if_not_computing text f x =
| Sys_error str ->
elt.analyzed_view#reset_initial;
elt.analyzed_view#set_message
- ("unable to communicate with coqtop, restarting coqtop:\n"^str)
+ ("Unable to communicate with coqtop, restarting coqtop.\n"^
+ "Error was: "^str)
| e ->
Mutex.unlock coq_computing;
elt.analyzed_view#set_message
@@ -537,7 +530,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
-let sup_args = ref ""
+let sup_args = ref []
class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct =
object(self)
@@ -2317,7 +2310,7 @@ let main files =
"_Start"
~tooltip:"Go to start"
~key:GdkKeysyms._Home
- ~callback:(do_or_activate (fun a -> a#reset_initial))
+ ~callback:force_reset_initial
`GOTO_TOP;
add_to_menu_toolbar
"_End"
diff --git a/ide/coqide.mli b/ide/coqide.mli
index cac6878cd..dd3995eb9 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -10,7 +10,7 @@
command line, initialize the load path, load the input
state, load the files given on the command line, load the ressource file,
produce the output state if any, and finally will launch the interface. *)
-val sup_args : string ref
+val sup_args : string list ref
val do_load : string -> unit
val process_argv : string list -> string list
val crash_save : int -> unit
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 6e36df6d1..4bb80f4a7 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -14,7 +14,7 @@ let () =
let argl = Array.to_list Sys.argv in
let files = Coqide.process_argv argl in
let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
- Coqide.sup_args := String.concat " " (List.map Filename.quote args);
+ Coqide.sup_args := List.map Filename.quote args;
Coq.check_connection !Coqide.sup_args;
Coqide.ignore_break ();
GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc");
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index a4c4b1d9f..ff8dbb2d6 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -582,6 +582,7 @@ let make_cases s : string list list call =
(* End of wrappers *)
let loop () =
+ Sys.catch_break true;
try
while true do
let q = (Marshal.from_channel: in_channel -> 'a call) stdin in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 22:04:58 +0000