From d70965923e50086e5f0bbba104da44750a982c64 Mon Sep 17 00:00:00 2001 From: monate Date: Tue, 20 May 2003 18:50:10 +0000 Subject: CoqIde: externals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4040 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/ideutils.ml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index e5edce660..4cf9c1ba2 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -240,3 +240,24 @@ let rec print_list print fmt = function | [] -> () | [x] -> print fmt x | x :: r -> print fmt x; print_list print fmt r + + +let run_command f c = + let result = Buffer.create 127 in + let cin,cout,cerr = Unix.open_process_full c [||] in + let buff = String.make 127 ' ' in + let buffe = String.make 127 ' ' in + let n = ref 0 in + let ne = ref 0 in + + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; + !n+ !ne <> 0 + do + let r = String.sub buff 0 !n in + f r; + Buffer.add_string result r; + let r = String.sub buffe 0 !ne in + f r; + Buffer.add_string result r + done; + (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) -- cgit v1.2.3