diff options
Diffstat (limited to 'ide')
| -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 |
5 files changed, 40 insertions, 9 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 |