Déplacement de fonctionnalités unix et browser de ide vers lib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 241477e8c4..7e59a876e0 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -218,6 +218,26 @@ let connect writefun readfun com =
   unlink tmp_to;
   a
 
+let run_command converter f c =
+  let result = Buffer.create 127 in
+  let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) 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 = converter (String.sub buff 0 !n) in 
+    f r;
+    Buffer.add_string result r;
+    let r = converter (String.sub buffe 0 !ne) in 
+    f r;
+    Buffer.add_string result r 
+  done;
+  (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
+
 (* Time stamps. *)
 
 type time = float * float * float