Tried to make F1 documentation tool working in CoqIDE.

In trunk: New strategy for compiling and finding index_url.txt. After
all, this file is not specific to CoqIDE but to the
documentation. Hence, it seems better to install it close to the
documentation. If the documentation is locally installed, it is easy
to find the file index_url.txt but what to do if the documentation is
remote? We would need a http getter. Does this mean we have to rely on
wget or so? In the absence of answer to this question, it seems
reasonable, first to assume the doc to be locally installed, second to
have a local copy of index_url.txt ready in the installation directory
of CoqIDE.
Also added an "automatic" field in the CoqIDE url preference to
prevent the user to have to update his preference file every time a
new version of Coq is out and the link to the doc change.

In 8.2: Added a minima the installation of index_urls.txt but the user
will have to update its preferences because the links
"http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer
exist.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 60 insertions, 13 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 01aef20fcd..ed52262af1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3127,7 +3127,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					    ~callback:
 					    (fun () -> 
 					       let av = session_notebook#current_term.analyzed_view in 
-						 browse av#insert_message (!current.doc_url)) in
+						 browse av#insert_message (doc_url ())) in
 					  let _ = help_factory#add_item "Browse Coq _Library" 
 					    ~callback:
 					    (fun () -> 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index dec23e36d9..ebf789fb37 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -312,10 +312,31 @@ let browse f url =
     f ("Could not execute\n\""^com^
        "\"\ncheck your preferences for setting a valid browser command\n")
 
+let doc_url () =
+  if !current.doc_url = use_default_doc_url || !current.doc_url = "" then 
+    if Sys.file_exists
+      (String.sub Coq_config.localwwwrefman 7
+	(String.length Coq_config.localwwwrefman - 7))
+    then
+      Coq_config.localwwwrefman
+    else
+      Coq_config.wwwrefman
+  else !current.doc_url
+
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
+  lazy (
   begin try
-    let cin = open_in (lib_ide_file "index_urls.txt") in
+    let cin = 
+      try open_in (lib_ide_file "index_urls.txt")
+      with _ ->
+	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
+    in
     try while true do
       let s = input_line cin in
       try 
@@ -324,18 +345,20 @@ let url_for_keyword =
 	let u = String.sub s (i + 1) (String.length s - i - 1) in
 	Hashtbl.add ht k u
       with _ ->
-	()
+	Printf.eprintf "Warning: Cannot parse documentation index file.\n";
+	flush stderr
     done with End_of_file ->
       close_in cin
   with _ ->
-    ()
+    Printf.eprintf "Warning: Cannot find documentation index file.\n";
+    flush stderr
   end;
-  (Hashtbl.find ht : string -> string)
+  Hashtbl.find ht : string -> string)
 
 
 let browse_keyword f text = 
-  try let u = url_for_keyword text in browse f (!current.doc_url ^ u) 
-  with Not_found -> f ("No documentation found for "^text)
+  try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) 
+  with Not_found -> f ("No documentation found for \""^text^"\".\n")
 
 
 (*
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1816ebcd9b..fbd5af44ea 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -14,6 +14,7 @@ val sync  : ('a -> 'b) -> 'a -> 'b
 (* avoid running two instances of a function concurrently *)
 val mutex : string -> ('a -> unit) -> 'a -> unit
 
+val doc_url : unit -> string
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
 val byte_offset_to_char_offset : string -> int -> int
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 0478978837..daa3839e06 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -101,6 +101,8 @@ type pref =
       mutable opposite_tabs : bool;
 }
 
+let use_default_doc_url = "(automatic)"
+
 let (current:pref ref) = 
   ref {
     cmd_coqc = "coqc";
@@ -224,7 +226,6 @@ let save_pref () =
     add "opposite_tabs" [string_of_bool p.opposite_tabs] ++
     Config_lexer.print_file pref_file
   with _ -> prerr_endline "Could not save preferences."
- 
 
 let load_pref () =
   (try GtkData.AccelMap.load accel_file with _ -> ());
@@ -269,7 +270,10 @@ let load_pref () =
     set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v);
     set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v);
     set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
-    set_hd "doc_url" (fun v -> np.doc_url <- v);
+    set_hd "doc_url" (fun v ->
+      if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url then
+	prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v);
+      np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
     set_bool "show_toolbar" (fun v -> np.show_toolbar <- v);
     set_bool "contextual_menus_on_goal" 
@@ -535,11 +539,28 @@ let configure ?(apply=(fun () -> ())) () =
                    else !current.cmd_browse])
       !current.cmd_browse
   in    
-  let doc_url = 
-    string ~f:(fun s -> !current.doc_url <- s) " Manual URL"  !current.doc_url in
+  let doc_url =
+    let predefined = [
+      use_default_doc_url
+    ] in
+    combo
+      "Manual URL"
+      ~f:(fun s -> !current.doc_url <- s)
+      ~new_allowed: true
+      (predefined@[if List.mem !current.doc_url predefined then ""
+                   else !current.doc_url])
+      !current.doc_url in
   let library_url = 
-    string ~f:(fun s -> !current.library_url <- s) "Library URL"  !current.library_url in
-
+    let predefined = [
+      Coq_config.wwwstdlib
+    ] in
+    combo
+      "Library URL"
+      ~f:(fun s -> !current.library_url <- s)
+      (predefined@[if List.mem !current.library_url predefined then ""
+                   else !current.library_url])
+      !current.library_url
+  in
   let automatic_tactics = 
     strings
       ~f:(fun l -> !current.automatic_tactics <- l) 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1f99cd9726..2094443b40 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -71,3 +71,5 @@ val change_font : ( Pango.font_description -> unit) ref
 val show_toolbar : (bool -> unit) ref
 val auto_complete : (bool -> unit) ref
 val resize_window : (unit -> unit) ref
+
+val use_default_doc_url : string