From 6af2902ddd8ea6d4171b882726e9bb4d2fc45748 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 14 Aug 2009 14:02:23 +0000 Subject: 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 --- Makefile.doc | 10 +++++++--- config/coq_config.mli | 1 + configure | 11 ++++++----- ide/coqide.ml | 2 +- ide/ideutils.ml | 35 +++++++++++++++++++++++++++++------ ide/ideutils.mli | 1 + ide/preferences.ml | 33 +++++++++++++++++++++++++++------ ide/preferences.mli | 2 ++ lib/flags.ml | 9 +++++++++ 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@.*\(.*\).*, .*@\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@.*\(.*\).*, .*@\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 diff --git a/configure b/configure index 0187e1f21..9daba918c 100755 --- a/configure +++ b/configure @@ -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 -- cgit v1.2.3