forked from xavierleroy/coq2html
-
Notifications
You must be signed in to change notification settings - Fork 4
Expand file tree
/
Copy pathcommand.ml
More file actions
58 lines (52 loc) · 1.5 KB
/
command.ml
File metadata and controls
58 lines (52 loc) · 1.5 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
open Common
let send o input =
output_string o input; flush o
let read_available ?(max=4096) ch =
let fd = Unix.descr_of_in_channel ch in
let ready, _, _ = Unix.select [fd] [] [] 0.1 in
if ready <> [] then begin
let rec iter store =
let buf = Bytes.create max in
let len = input ch buf 0 max in
if len < max then
let s = Bytes.sub_string buf 0 len in
String.concat "" @@ List.rev (s :: store)
else
let s = Bytes.to_string buf in
iter (s :: store)
in
Some (iter [])
end
else None
let input_line_with_timeout timeout_sec ch =
let fd = Unix.descr_of_in_channel ch in
let ready, _, _ = Unix.select [fd] [] [] timeout_sec in
if ready = [] then (* Timeout *)
None
else
Some (input_line ch)
let show_errors (i, o, e) =
match read_available e with
| Some msg -> Log.warn msg
| None -> ()
let close command ioe =
show_errors ioe;
match Unix.close_process_full ioe with
| Unix.WEXITED 0 -> ()
| WEXITED other ->
Log.warn (!%"Command '%s': exit %d" command other)
| WSIGNALED signal ->
Log.warn (!%"Command '%s': killed by a signal:%d" command signal)
| WSTOPPED signal ->
Log.warn (!%"Command '%s': stopped by a signal:%d" command signal)
let using command f =
let env = Unix.environment () in
let (i, o, e) = Unix.open_process_full command env in
try
let y = f (i, o, e) in
close command (i, o, e);
y
with
| exn ->
close command (i, o, e);
raise exn