[ide] only use Coq_config for the URL of the manual

5 files changed, 5 insertions, 76 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 48c08899e0..94778e0c60 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1182,10 +1182,10 @@ let build_ui () =
     item "Help" ~label:"_Help";
     item "Browse Coq Manual" ~label:"Browse Coq _Manual"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#default_route#add_string (doc_url ()));
+        browse notebook#current_term.messages#default_route#add_string Coq_config.wwwrefman);
     item "Browse Coq Library" ~label:"Browse Coq _Library"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#default_route#add_string library_url#get);
+        browse notebook#current_term.messages#default_route#add_string Coq_config.wwwstdlib);
     item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
       ~callback:(fun _ -> on_current_term (fun sn ->
         browse_keyword sn.messages#default_route#add_string (get_current_word sn)));
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c14af7d21d..5beaba3604 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -458,15 +458,6 @@ let browse prerr url =
   in
   run_command (fun _ -> ()) finally com
 
-let doc_url () =
-  if doc_url#get = use_default_doc_url || doc_url#get = ""
-  then
-    let addr = List.fold_left Filename.concat (Envars.docdir ())
-      ["html";"refman";"index.html"]
-    in
-    if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
-  else doc_url#get
-
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
     lazy (
@@ -476,13 +467,7 @@ let url_for_keyword =
             (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
             (Minilib.coqide_data_dirs ())) "index_urls.txt" in
             open_in index_urls
-          with Not_found ->
-            let doc_url = doc_url () in
-            let n = String.length doc_url in
-              if n > 8 && String.sub doc_url 0 7 = "file://" then
-                open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt")
-              else
-                raise Exit
+          with Not_found -> raise Exit
         in
           try while true do
             let s = input_line cin in
@@ -503,7 +488,7 @@ let url_for_keyword =
 let browse_keyword prerr text =
   try
     let u = Lazy.force url_for_keyword text in
-    browse prerr (doc_url() ^ u)
+    browse prerr (Coq_config.wwwrefman ^ u)
   with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
 
 let rec is_valid (s : Pp.t) = match Pp.repr s with
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 0031c59c17..531c71cd4b 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -13,7 +13,6 @@ val warning : string -> unit
 
 val cb : GData.clipboard
 
-val doc_url : unit -> string
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4aa8c92f73..e6ec5f52c8 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -366,33 +366,6 @@ let text_font =
   in
   new preference ~name:["text_font"] ~init ~repr:Repr.(string)
 
-let is_standard_doc_url url =
-  let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
-  let n = String.length Coq_config.wwwcoq in
-  let n' = String.length Coq_config.wwwrefman in
-  url = Coq_config.localwwwrefman ||
-  url = Coq_config.wwwrefman ||
-  url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
-
-let doc_url =
-object
-  inherit [string] preference
-    ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
-    as super
-
-  method! set v =
-    if not (is_standard_doc_url v) &&
-      v <> use_default_doc_url &&
-      (* Extra hack to support links to last released doc version *)
-      v <> Coq_config.wwwcoq ^ "doc" &&
-      v <> Coq_config.wwwcoq ^ "doc/"
-    then super#set v
-
-end
-
-let library_url =
-  new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string)
-
 let show_toolbar =
   new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
 
@@ -948,32 +921,6 @@ let configure ?(apply=(fun () -> ())) parent =
                    else cmd_browse#get])
       cmd_browse#get
   in
-  let doc_url =
-    let predefined = [
-      "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]);
-      Coq_config.wwwrefman;
-      use_default_doc_url
-    ] in
-    combo
-      "Manual URL"
-      ~f:doc_url#set
-      ~new_allowed: true
-      (predefined@[if List.mem doc_url#get predefined then ""
-                   else doc_url#get])
-      doc_url#get in
-  let library_url =
-    let predefined = [
-      "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]);
-      Coq_config.wwwstdlib
-    ] in
-    combo
-      "Library URL"
-      ~f:(fun s -> library_url#set s)
-      ~new_allowed: true
-      (predefined@[if List.mem library_url#get predefined then ""
-                   else library_url#get])
-      library_url#get
-  in
   let automatic_tactics =
     strings
       ~f:automatic_tactics#set
@@ -1039,7 +986,7 @@ let configure ?(apply=(fun () -> ())) parent =
      Section("Appearance", Some `PREFERENCES, [window_width; window_height]);
      Section("Externals", None,
 	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
-	      cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
+              cmd_print;cmd_editor;cmd_browse]);
      Section("Tactics Wizard", None,
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 7ed6a40bdb..cf2265781c 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -74,8 +74,6 @@ val modifiers_valid : string preference
 val cmd_browse : string preference
 val cmd_editor : string preference
 val text_font : string preference
-val doc_url : string preference
-val library_url : string preference
 val show_toolbar : bool preference
 val contextual_menus_on_goal : bool preference
 val window_width : int preference