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

2 files changed, 11 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))