diff options
Diffstat (limited to 'ide')
| -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 |
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 |