diff options
| -rw-r--r-- | Makefile.doc | 10 | ||||
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 11 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/ideutils.ml | 35 | ||||
| -rw-r--r-- | ide/ideutils.mli | 1 | ||||
| -rw-r--r-- | ide/preferences.ml | 33 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 9 | ||||
| -rw-r--r-- | lib/flags.mli | 4 |
10 files changed, 86 insertions, 22 deletions
diff --git a/Makefile.doc b/Makefile.doc index e5822eb5b..5388c6769 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -258,15 +258,15 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex # Not robust, improve... ide/index_urls.txt: doc/refman/html/index.html - @ rm -f ide/index_urls.txt - cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt + @ rm -f doc/refman/html/index_urls.txt + cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > doc/refman/html/index_urls.txt ###################################################################### # Install all documentation files ###################################################################### -install-doc: install-doc-meta install-doc-html install-doc-printable +install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-url install-doc-meta: $(MKDIR) $(FULLDOCDIR) @@ -293,6 +293,10 @@ install-doc-printable: $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps +install-doc-index-url: + $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf + $(INSTALLLIB) doc/refman/html/index_urls.txt \ + $(FULLDOCDIR)/html/refman # For emacs: # Local Variables: diff --git a/config/coq_config.mli b/config/coq_config.mli index 5294ee6f1..2cd1e4543 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -67,4 +67,5 @@ val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *) val wwwcoq : string val wwwrefman : string val wwwstdlib : string +val localwwwrefman : string @@ -371,7 +371,7 @@ if [ "$browser_spec" = "no" ]; then fi if [ "$wwwcoq_spec" = "no" ]; then - WWWCOQ="http://www.lix.polytechnique.fr/coq/" + WWWCOQ="http://coq.inria.fr/" fi ######################################### @@ -759,13 +759,13 @@ case $mandir_spec/$prefix_spec/$local in esac case $docdir_spec/$prefix_spec/$local in - yes/*/*) DOCDIR=$docdir;; - */yes/*) DOCDIR=$prefix/share/doc/coq ;; - */*/true) DOCDIR=$COQTOP/man ;; + yes/*/*) DOCDIR=$docdir; HTMLREFMANDIR=$DOCDIR/html/refman;; + */yes/*) DOCDIR=$prefix/share/doc/coq; HTMLREFMANDIR=$DOCDIR/html/refman;; + */*/true) DOCDIR=$COQTOP/doc; HTMLREFMANDIR=$DOCDIR/refman/html;; *) printf "Where should I install the Coq documentation [$docdir_def]? " read DOCDIR case $DOCDIR in - "") DOCDIR=$docdir_def;; + "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;; *) true;; esac;; esac @@ -1019,6 +1019,7 @@ let browser = "$BROWSER" let wwwcoq = "$WWWCOQ" let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/" let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/" +let localwwwrefman = "file://$HTMLREFMANDIR/" END_OF_COQ_CONFIG diff --git a/ide/coqide.ml b/ide/coqide.ml index 01aef20fc..ed52262af 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 dec23e36d..ebf789fb3 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 1816ebcd9..fbd5af44e 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 047897883..daa3839e0 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 1f99cd972..2094443b4 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 diff --git a/lib/flags.ml b/lib/flags.ml index c0af148c7..dac88a473 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -102,6 +102,15 @@ let browser_cmd_fmt = with Not_found -> Coq_config.browser +let is_standard_doc_url url = + let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in + let wwwprefix = "http://coq.inria.fr/" in + let n = String.length wwwprefix 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) + (* Options for changing coqlib *) let coqlib_spec = ref false let coqlib = ref Coq_config.coqlib diff --git a/lib/flags.mli b/lib/flags.mli index fe1157d88..8bafa8b1f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -70,7 +70,9 @@ val boxed_definitions : unit -> bool (* Returns string format for default browser to use from Coq or CoqIDE *) val browser_cmd_fmt : string - + +val is_standard_doc_url : string -> bool + (* Substitute %s in the first chain by the second chain *) val subst_command_placeholder : string -> string -> string |