diff options
-rw-r--r-- | ide/coq.ml | 30 | ||||
-rw-r--r-- | ide/coqide.ml | 4 | ||||
-rw-r--r-- | ide/fileOps.ml | 2 | ||||
-rw-r--r-- | ide/ideutils.ml | 11 | ||||
-rw-r--r-- | ide/ideutils.mli | 2 | ||||
-rw-r--r-- | lib/flags.ml | 2 | ||||
-rw-r--r-- | lib/flags.mli | 2 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
-rw-r--r-- | toplevel/ide_slave.ml | 9 | ||||
-rw-r--r-- | toplevel/stm.ml | 55 |
10 files changed, 99 insertions, 24 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 5d8efebd1..8442493b4 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -327,7 +327,7 @@ let lift (f : unit -> 'a) : 'a task = closed in coqide. *) -let open_process_pid prog args = +let open_coqtop_pipe 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; @@ -343,6 +343,34 @@ let open_process_pid prog args = Unix.out_channel_of_descr ide2top_w, (fun () -> Unix.close top2ide_r; Unix.close ide2top_w) +let open_coqtop_socket prog args = + let s = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in + Unix.bind s (Unix.ADDR_INET (Unix.inet_addr_loopback,0)); + Unix.listen s 1; + let host, port = + match Unix.getsockname s with + | Unix.ADDR_INET(host, port) -> + Unix.string_of_inet_addr host, string_of_int port + | _ -> assert false in + let pid = + Unix.create_process prog + (Array.append args [|"-ideslave-socket";host^":"^port|]) + (Unix.openfile "slave.in" [Unix.O_CREAT;Unix.O_RDONLY] 0o660) + (Unix.openfile "slave.out" [Unix.O_CREAT;Unix.O_WRONLY] 0o660) + (Unix.openfile "slave.err" [Unix.O_CREAT;Unix.O_WRONLY] 0o660) in + assert (pid <> 0); + let cs, _ = Unix.accept s in + Unix.set_nonblock cs; + pid, + Unix.in_channel_of_descr cs, + Glib.Io.channel_of_descr_socket cs, + Unix.out_channel_of_descr cs, + (fun () -> Unix.close cs; Unix.close s) + +let open_process_pid prog args = + if Sys.os_type = "Unix" then open_coqtop_pipe prog args + else open_coqtop_socket prog args + exception TubeError exception AnswerWithoutRequest of string diff --git a/ide/coqide.ml b/ide/coqide.ml index 5b2ca6f8b..b223be3a4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -171,7 +171,7 @@ let check_quit saveall = "Quit without Saving"; "Don't Quit"] ~default:0 - ~icon:warn_image#coerce + ~icon:(warn_image ())#coerce "There are unsaved buffers" in match answ with @@ -259,7 +259,7 @@ let close_buffer sn = "Close without Saving"; "Don't Close"] ~default:0 - ~icon:warn_image#coerce + ~icon:(warn_image ())#coerce "This buffer has unsaved modifications" in match answ with diff --git a/ide/fileOps.ml b/ide/fileOps.ml index a1066db2c..3b8599818 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.ml @@ -108,7 +108,7 @@ object(self) let answ = GToolbox.question_box ~title:"File exists on disk" ~buttons:["Overwrite"; "Cancel";] ~default:1 - ~icon:warn_image#coerce + ~icon:(warn_image ())#coerce ("File "^f^" already exists") in match answ with diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 881f5ea43..2ae46fc7e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -11,14 +11,14 @@ open Preferences exception Forbidden -let warn_image = +let warn_image () = let img = GMisc.image () in img#set_stock `DIALOG_WARNING; img#set_icon_size `DIALOG; img -let warning msg = - GToolbox.message_box ~title:"Warning" ~icon:warn_image#coerce msg +let warning msg = + GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg let cb = GData.clipboard Gdk.Atom.primary @@ -328,7 +328,10 @@ let io_read_all chan = let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in Buffer.add_substring read_buffer read_string 0 len in - begin try while true do read_once () done with _ -> () end; + begin + try while true do read_once () done + with Glib.GError _ -> () + end; Buffer.contents read_buffer (** Run an external command asynchronously *) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index bb9e65322..5fd97e3a5 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val warn_image : GMisc.image +val warn_image : unit -> GMisc.image val warning : string -> unit val cb : GData.clipboard diff --git a/lib/flags.ml b/lib/flags.ml index cde45a81f..b79f80d22 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -45,7 +45,6 @@ let boot = ref false let batch_mode = ref false -let ide_slave_mode = ref false let coq_slave_mode = ref (-1) let coq_slaves_number = ref 1 @@ -60,6 +59,7 @@ let term_quality = ref false let xml_export = ref false let ide_slave = ref false +let ide_slave_socket = ref None let time = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 8525d731b..0b7adf33f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -12,7 +12,6 @@ val boot : bool ref val batch_mode : bool ref -val ide_slave_mode : bool ref val coq_slave_mode : int ref val coq_slaves_number : int ref @@ -27,6 +26,7 @@ val term_quality : bool ref val xml_export : bool ref val ide_slave : bool ref +val ide_slave_socket : (string * int) option ref val time : bool ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f3bcee128..a0de42bf6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -233,6 +233,11 @@ let get_int opt n = with Failure _ -> prerr_endline ("Error: integer expected after option "^opt); exit 1 +let get_host_port opt s = + match CString.split ':' s with + | [host; port] -> Some (host, int_of_string port) + | _ -> prerr_endline ("Error: host:port expected after option "^opt); exit 1 + let parse_args arglist = let args = ref arglist in let extras = ref [] in @@ -272,6 +277,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-exclude-dir" -> exclude_search_in_dirname (next ()) + |"-ideslave-socket" -> Flags.ide_slave_socket := get_host_port opt (next()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index be384e174..98386c69e 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -401,8 +401,13 @@ let slave_feeder xml_oc msg = let loop () = init_signal_handler (); catch_break := false; - let xml_oc = Xml_printer.make (Xml_printer.TChannel !orig_stdout) in - let xml_ic = Xml_parser.make (Xml_parser.SChannel stdin) in + let in_ch, out_ch = + match !Flags.ide_slave_socket with + | None -> stdin, !orig_stdout + | Some(h,p) -> + Unix.open_connection (Unix.ADDR_INET(Unix.inet_addr_of_string h,p)) in + let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in + let xml_ic = Xml_parser.make (Xml_parser.SChannel in_ch) in let () = Xml_parser.check_eof xml_ic false in set_logger (slave_logger xml_oc); set_feeder (slave_feeder xml_oc); diff --git a/toplevel/stm.ml b/toplevel/stm.ml index ea9a85f51..5f1c31e42 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -7,9 +7,10 @@ (************************************************************************) let prerr_endline s = - if !Flags.debug then - prerr_endline (Printf.sprintf "%d] %s" !Flags.coq_slave_mode s) - else () + if !Flags.debug then begin + prerr_endline (Printf.sprintf "%d] %s" !Flags.coq_slave_mode s); + flush stderr + end else () open Vernacexpr open Errors @@ -654,6 +655,16 @@ end = struct (* {{{ *) | Some managers -> Array.length managers let is_empty () = !slave_managers = None + let master_handshake ic oc = + try + Marshal.to_channel oc 17 []; flush oc; + let n = (Marshal.from_channel ic : int) in + assert(n = 17); + prerr_endline "Handshake OK" + with e -> + prerr_endline ("Handshake failed: "^Printexc.to_string e); + exit 1 + let respawn n () = let c2s_r, c2s_w = Unix.pipe () in let s2c_r, s2c_w = Unix.pipe () in @@ -674,7 +685,12 @@ end = struct (* {{{ *) let pid = Unix.create_process_env prog args env c2s_r s2c_w Unix.stderr in Unix.close c2s_r; Unix.close s2c_w; - Unix.in_channel_of_descr s2c_r, Unix.out_channel_of_descr c2s_w, pid, n + let s2c_r = Unix.in_channel_of_descr s2c_r in + let c2s_w = Unix.out_channel_of_descr c2s_w in + set_binary_mode_out c2s_w true; + set_binary_mode_in s2c_r true; + master_handshake s2c_r c2s_w; + s2c_r, c2s_w, pid, n let init n manage_slave = slave_managers := Some @@ -763,11 +779,13 @@ end = struct (* {{{ *) let marshal_request oc (req : request) = try marshal_to_channel oc req - with Failure s | Invalid_argument s -> marshal_err ("marshal_request: "^s) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("marshal_request: "^s) let unmarshal_request ic = try (Marshal.from_channel ic : request) - with Failure s | Invalid_argument s -> marshal_err ("unmarshal_request: "^s) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_request: "^s) (* Since cancelling is still cooperative, the slave runs a thread that periodically sends a RespTick message on the same channel used by the @@ -778,20 +796,23 @@ end = struct (* {{{ *) fun oc (res : response) -> Mutex.lock m; try marshal_to_channel oc res; Mutex.unlock m - with Failure s | Invalid_argument s -> + with Failure s | Invalid_argument s | Sys_error s -> Mutex.unlock m; marshal_err ("marshal_response: "^s) let unmarshal_response ic = try (Marshal.from_channel ic : response) - with Failure s | Invalid_argument s -> marshal_err ("unmarshal_response: "^s) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_response: "^s) let marshal_more_data oc (res : more_data) = try marshal_to_channel oc res - with Failure s | Invalid_argument s -> marshal_err ("marshal_more_data: "^s) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("marshal_more_data: "^s) let unmarshal_more_data ic = try (Marshal.from_channel ic : more_data) - with Failure s | Invalid_argument s -> marshal_err ("unmarshal_more_data: "^s) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_more_data: "^s) let queue : task TQueue.t = TQueue.create () @@ -823,7 +844,8 @@ end = struct (* {{{ *) let rec manage_slave respawn = let ic, oc, pid, id_slave = respawn () in let kill_pid = - ref (fun () -> try Unix.kill pid 9 with Unix.Unix_error _ -> ()) in + ref (fun () -> try Unix.kill pid 9 + with Unix.Unix_error _ | Invalid_argument _ -> ()) in at_exit (fun () -> !kill_pid ()); let last_task = ref None in try @@ -940,6 +962,16 @@ end = struct (* {{{ *) | [] -> let data = f () in l := List.tl data; List.hd data | x::tl -> l := tl; x + let slave_handshake () = + try + let v = (Marshal.from_channel !slave_ic : int) in + assert(v = 17); + Marshal.to_channel !slave_oc v []; flush !slave_oc; + prerr_endline "Handshake OK" + with e -> + prerr_endline ("Handshake failed: " ^ Printexc.to_string e); + exit 1 + let slave_main_loop reset = let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; @@ -959,6 +991,7 @@ end = struct (* {{{ *) Unix.sleep n; if !working then marshal_response !slave_oc RespTick done) 1 in + slave_handshake (); while true do try working := false; |