aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorEnrico Tassi2014-02-10 15:38:58 +0100
committerEnrico Tassi2014-02-10 18:04:10 +0100
commit41845e6d4334eeaa7addf6b11f6cb4cda5a7f8cc (patch)
tree6f96af6235de9141185252369baa4acdbc4d28c5 /tools
parentcee357d2457295473dfe5ca4ebd8948bb7bca498 (diff)
fake_ide: ported to spawn
Diffstat (limited to 'tools')
-rw-r--r--tools/fake_ide.ml14
1 files changed, 10 insertions, 4 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 5b6db94a43..6567c2fe21 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -289,17 +289,23 @@ let usage () =
(Filename.basename Sys.argv.(0))
(Parser.print grammar))
+module Coqide = Spawn.Sync(struct
+ let add_timeout ~sec:_ _ = ()
+end)
+
let main =
Sys.set_signal Sys.sigpipe
(Sys.Signal_handle
(fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
- let coqtop_name, input_file = match Sys.argv with
- | [| _; f |] -> "coqtop", f
- | [| _; f; ct |] -> ct, f
+ let coqtop_name, coqtop_args, input_file = match Sys.argv with
+ | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+ | [| _; f; ct |] ->
+ let ct = Str.split (Str.regexp " ") ct in
+ List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
| _ -> usage () in
let inc = if input_file = "-" then stdin else open_in input_file in
let coq =
- let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in
+ let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in
let ip = Xml_parser.make (Xml_parser.SChannel cin) in
let op = Xml_printer.make (Xml_printer.TChannel cout) in
Xml_parser.check_eof ip false;