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

4 files changed, 40 insertions, 0 deletions

diff --git a/lib/options.ml b/lib/options.ml
index f190519f1..45f27107e 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -117,3 +117,10 @@ let boxed_definitions = ref true
 let set_boxed_definitions b = boxed_definitions := b
 let boxed_definitions _ = !boxed_definitions 
  
+(* Options for external tools *)
+
+let browser_cmd_fmt =
+  if Sys.os_type = "Win32"
+  then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
+  else "netscape -remote \"OpenURL(", ")\""
+  
diff --git a/lib/options.mli b/lib/options.mli
index 1c0779950..6b28158c3 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -70,4 +70,9 @@ val print_bytecodes : unit -> bool
 val set_boxed_definitions : bool -> unit
 val boxed_definitions : unit -> bool
 
+(* Options for external tools *)
+
+(* Returns head and tail of printf string format *)
+(* ocaml doesn't allow not applied formats *)
+val browser_cmd_fmt : string * string
  
diff --git a/lib/system.ml b/lib/system.ml
index 241477e8c..7e59a876e 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
diff --git a/lib/system.mli b/lib/system.mli
index 40bacdec0..1ecd4bcff 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -50,6 +50,14 @@ val extern_intern :
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a 
 
+(*s [run_command converter f com] launches command [com], and returns
+    the contents of stdout and stderr that have been processed with
+    [converter]; the processed contents of stdout and stderr is also
+    passed to [f] *)
+
+val run_command : (string -> string) -> (string -> unit) -> string -> 
+  Unix.process_status * string
+
 (*s Time stamps. *)
 
 type time