diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 02:28:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-01 05:00:01 +0200 |
| commit | 4de95593380294b3d2c4f10f346aaf9bb5d4d6eb (patch) | |
| tree | e65e843f7bd461348be11369efb7b28d84dc2cb7 /ide | |
| parent | c403fa491bb4ef9710c6251e5d5c47c046c95e39 (diff) | |
[lib] [flags] Move private IDE functions to `ide`
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/preferences.ml | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 955ee87840..3f10af04c9 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -345,8 +345,15 @@ let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" let modifiers_valid = new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string) +let browser_cmd_fmt = + try + let coq_netscape_remote_var = "COQREMOTEBROWSER" in + Sys.getenv coq_netscape_remote_var + with + Not_found -> Coq_config.browser + let cmd_browse = - new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string) + new preference ~name:["cmd_browse"] ~init:browser_cmd_fmt ~repr:Repr.(string) let cmd_editor = let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in @@ -359,6 +366,14 @@ 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 @@ -366,7 +381,7 @@ object as super method! set v = - if not (Flags.is_standard_doc_url 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" && |