1
(**************************************************************************)
5
(* Fran�ois Pottier, INRIA Rocquencourt *)
6
(* Yann R�gis-Gianas, PPS, Universit� Paris Diderot *)
8
(* Copyright 2005-2008 Institut National de Recherche en Informatique *)
9
(* et en Automatique. All rights reserved. This file is distributed *)
10
(* under the terms of the Q Public License version 1.0, with the change *)
11
(* described in file LICENSE. *)
13
(**************************************************************************)
15
(* Input-output utilities. *)
17
(* ------------------------------------------------------------------------- *)
18
(* [exhaust channel] reads all of the data that's available on [channel]. *)
24
let buffer = Buffer.create chunk_size in
25
let chunk = String.create chunk_size in
27
let length = input channel chunk 0 chunk_size in
29
Buffer.contents buffer
31
Buffer.add_substring buffer chunk 0 length;
37
(* ------------------------------------------------------------------------- *)
38
(* [invoke command] invokes an external command (which expects no
39
input) and returns its output, if the command succeeds. It returns
40
[None] if the command fails. *)
43
let ic = Unix.open_process_in command in
44
let result = exhaust ic in
45
match Unix.close_process_in ic with
51
(* ------------------------------------------------------------------------- *)
52
(* [winvoke writers command cleaners] invokes each of the [writer]
53
functions, invokes the command [command], and runs each of the
54
[cleaner] functions. Then, it either returns the command's output,
55
if the command succeeded, or exits, otherwise. *)
57
let winvoke writers command cleaners =
61
List.iter call writers;
62
let output = invoke command in
63
List.iter call cleaners;
65
(* Stop if the command failed. Otherwise, return its output. *)
69
(* Presumably, the command printed an error message for us. *)