From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- ide/coq.ml | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index 8b1fa0a3..07f0ece8 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -191,11 +191,29 @@ let coqtop_zombies () = Note: we use Unix.stderr in Unix.create_process to get debug messages from the coqtop's Ide_slave loop. + + NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r) + in coqtop. We do this indirectly via [Unix.set_close_on_exec]. + This way, coqide has the only remaining copies of these descriptors, + and closing them later will have visible effects in coqtop. Cf man 7 pipe : + + - If all file descriptors referring to the write end of a pipe have been + closed, then an attempt to read(2) from the pipe will see end-of-file + (read(2) will return 0). + - If all file descriptors referring to the read end of a pipe have been + closed, then a write(2) will cause a SIGPIPE signal to be generated for + the calling process. If the calling process is ignoring this signal, + then write(2) fails with the error EPIPE. + + Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be + closed in coqide. *) let open_process_pid prog args = let (ide2top_r,ide2top_w) = Unix.pipe () in let (top2ide_r,top2ide_w) = Unix.pipe () in + Unix.set_close_on_exec ide2top_w; + Unix.set_close_on_exec top2ide_r; let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in assert (pid <> 0); Unix.close ide2top_r; @@ -250,7 +268,7 @@ let eval_call coqtop (c:'a Ide_intf.call) = Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c); flush coqtop.cin; let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in - (Ide_intf.to_answer xml : 'a Interface.value) + (Ide_intf.to_answer xml c : 'a Interface.value) let interp coqtop ?(raw=false) ?(verbose=true) s = eval_call coqtop (Ide_intf.interp (raw,verbose,s)) -- cgit v1.2.3