diff options
| author | Enrico Tassi | 2014-02-10 15:38:58 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-02-10 18:04:10 +0100 |
| commit | 41845e6d4334eeaa7addf6b11f6cb4cda5a7f8cc (patch) | |
| tree | 6f96af6235de9141185252369baa4acdbc4d28c5 /tools | |
| parent | cee357d2457295473dfe5ca4ebd8948bb7bca498 (diff) | |
fake_ide: ported to spawn
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/fake_ide.ml | 14 |
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; |
