From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 ide/preferences.ml | 44 +++++++++++---------------------------------
 1 file changed, 11 insertions(+), 33 deletions(-)

(limited to 'ide/preferences.ml')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 8743b99b..8629fe8e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml,v 1.27.2.2 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: preferences.ml 7046 2005-05-20 07:38:25Z herbelin $ *)
 
 open Configwin
 open Printf
@@ -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))
-- 
cgit v1.2.3