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

6 files changed, 51 insertions, 53 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d048c3fd5a..e8cccf9ccf 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -226,29 +226,9 @@ let rec print_list print fmt = function
   | 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 (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 = try_convert (String.sub buff 0 !n) in 
-    f r;
-    Buffer.add_string result r;
-    let r = try_convert (String.sub buffe 0 !ne) in 
-    f r;
-    Buffer.add_string result r 
-  done;
-  (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
-
 let browse f url =
   let l,r = !current.cmd_browse in
-  let (s,res) = run_command f (l ^ url ^ r) in
+  let (s,res) = System.run_command try_convert f (l ^ url ^ r) in
   ()
 
 let url_for_keyword =
diff --git a/ide/preferences.ml b/ide/preferences.ml
index edae8e673f..3e4a335748 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -123,10 +123,7 @@ let (current:pref ref) =
     modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4];
 
     
-    cmd_browse = 
-	 if Sys.os_type = "Win32"
-	 then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
-	 else "netscape -remote \"OpenURL(", ")\"";
+    cmd_browse = Options.browser_cmd_fmt
     cmd_editor = 
 	 if Sys.os_type = "Win32"
 	 then "NOTEPAD ", ""
@@ -269,6 +266,13 @@ let load_pref () =
     prerr_endline ("Could not load preferences ("^
 		   (Printexc.to_string e)^").")
     
+let split_string_format s =
+  try 
+    let i = Util.string_index_from s 0 "%s" in
+    let pre = (String.sub s 0 i) in
+    let post = String.sub s (i+2) (String.length s - i - 2) in
+    pre,post
+  with Not_found -> s,""
 
 let configure () = 
   let cmd_coqc = 
@@ -439,40 +443,14 @@ let configure () =
 
   let cmd_editor = 
     string
-      ~f:(fun s -> 
-	    !current.cmd_editor <- 
-	    try 
-	      let i = String.index s '%' in
-	      let pre = (String.sub s 0 i) in
-	      if String.length s - 1 = i then 
-		pre,""
-	      else
-		let post = String.sub s (i+2) (String.length s - i - 2) in
-		prerr_endline pre;
-		prerr_endline post;
-		pre,post
-	    with Not_found -> s,""
-	    )
+      ~f:(fun s -> !current.cmd_editor <- split_string_format s)
       ~help:"(%s for file name)" 
       "External editor"
       ((fst !current.cmd_editor)^"%s"^(snd !current.cmd_editor))
   in    
   let cmd_browse = 
     string
-      ~f:(fun s -> 
-	    !current.cmd_browse <- 
-	    try 
-	      let i = String.index s '%' in
-	      let pre = (String.sub s 0 i) in
-	      if String.length s - 1 = i then 
-		pre,""
-	      else
-		let post = String.sub s (i+2) (String.length s - i - 2) in
-		prerr_endline pre;
-		prerr_endline post;
-		pre,post
-	    with Not_found -> s,""
-	    )
+      ~f:(fun s -> !current.cmd_browse <- split_string_format s)
       ~help:"(%s for url)" 
       "    Browser"
       ((fst !current.cmd_browse)^"%s"^(snd !current.cmd_browse))
diff --git a/lib/options.ml b/lib/options.ml
index f190519f1f..45f27107e3 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 1c07799509..6b28158c3b 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 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
diff --git a/lib/system.mli b/lib/system.mli
index 40bacdec09..1ecd4bcffa 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