From 417ac448411ce924444915da8e7e6fb81a12bc57 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Nov 2016 11:11:20 +0100 Subject: Configuration: always giving a value to configdir and datadir. They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories. --- ide/minilib.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/minilib.ml b/ide/minilib.ml index 2c24e46f8..c9cef5639 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -54,12 +54,12 @@ let coqide_config_home () = let coqide_data_dirs () = coqify (Glib.get_user_data_dir ()) :: List.map coqify (Glib.get_system_data_dirs ()) - @ Option.List.cons Coq_config.datadir [] + @ [Coq_config.datadir] let coqide_config_dirs () = coqide_config_home () :: List.map coqify (Glib.get_system_config_dirs ()) - @ Option.List.cons Coq_config.configdir [] + @ [Coq_config.configdir] let is_prefix_of pre s = let i = ref 0 in -- cgit v1.2.3 From 5c875b6ab907cb48b0d06aba48d4c733cfd2ff06 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 04:01:29 +0100 Subject: Relying on computation done in Envars to discover the installation directories. This allows to share the test for possible relocalisation done in envars.ml. --- ide/ideutils.ml | 2 +- ide/minilib.ml | 4 ++-- ide/preferences.ml | 4 ++-- lib/envars.ml | 5 +++++ lib/envars.mli | 12 +++++++++--- 5 files changed, 19 insertions(+), 8 deletions(-) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index a08ab07b5..8a0e507c0 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -422,7 +422,7 @@ let browse prerr url = let doc_url () = if doc_url#get = use_default_doc_url || doc_url#get = "" then - let addr = List.fold_left Filename.concat (Coq_config.docdir) + let addr = List.fold_left Filename.concat (Envars.docdir ()) ["html";"refman";"index.html"] in if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman diff --git a/ide/minilib.ml b/ide/minilib.ml index c9cef5639..2b278fac6 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -54,12 +54,12 @@ let coqide_config_home () = let coqide_data_dirs () = coqify (Glib.get_user_data_dir ()) :: List.map coqify (Glib.get_system_data_dirs ()) - @ [Coq_config.datadir] + @ [Envars.datadir ()] let coqide_config_dirs () = coqide_config_home () :: List.map coqify (Glib.get_system_config_dirs ()) - @ [Coq_config.configdir] + @ [Envars.configdir ()] let is_prefix_of pre s = let i = ref 0 in diff --git a/ide/preferences.ml b/ide/preferences.ml index 9fe9c6337..d97e49927 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -918,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () = in let doc_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]); + "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]); Coq_config.wwwrefman; use_default_doc_url ] in @@ -931,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () = doc_url#get in let library_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]); + "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]); Coq_config.wwwstdlib ] in combo diff --git a/lib/envars.ml b/lib/envars.ml index 78f14273d..bc8012297 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -135,6 +135,11 @@ let datadir () = let path = use_suffix coqroot Coq_config.datadirsuffix in if Sys.file_exists path then path else Coq_config.datadir +let configdir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.configdirsuffix in + if Sys.file_exists path then path else Coq_config.configdir + let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in let make_search_path path = diff --git a/lib/envars.mli b/lib/envars.mli index c33a08c40..c8bbf17d9 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -27,12 +27,18 @@ val home : warn:(string -> unit) -> string (** [coqlib] is the path to the Coq library. *) val coqlib : unit -> string +(** [docdir] is the path to the installed documentation. *) +val docdir : unit -> string + +(** [datadir] is the path to the installed data directory. *) +val datadir : unit -> string + +(** [configdir] is the path to the installed config directory. *) +val configdir : unit -> string + (** [set_coqlib] must be runned once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit -(** [docdir] is the path to the Coq documentation. *) -val docdir : unit -> string - (** [coqbin] is the name of the current executable. *) val coqbin : string -- cgit v1.2.3