diff options
| -rw-r--r-- | lib/envars.ml | 4 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 23 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
6 files changed, 22 insertions, 17 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index b6312e7d9..a4629e50d 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -192,9 +192,9 @@ let camlp4lib () = (** {1 XDG utilities} *) -let xdg_data_home warning = +let xdg_data_home warn = coqify - (getenv_else "XDG_DATA_HOME" (fun () -> (home warning) / ".local/share")) + (getenv_else "XDG_DATA_HOME" (fun () -> (home ~warn) / ".local/share")) let xdg_config_home warn = coqify diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d42d612ae..aab237a23 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1759,7 +1759,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste Lazy.force require_csdp; let cmdname = - List.fold_left Filename.concat (Envars.coqlib Errors.error) + List.fold_left Filename.concat (Envars.coqlib ~fail:Errors.error) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 0373b82e9..76548aa3d 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -71,7 +71,7 @@ let src_dirs = [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"] ] let includes () = - let coqlib = if !Flags.boot then "." else Envars.coqlib Errors.error in + let coqlib = if !Flags.boot then "." else Envars.coqlib ~fail:Errors.error in let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs []) @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3b5034e95..1f4082b84 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -32,13 +32,16 @@ let load_rcfile() = if CUnix.file_readable_p !rcfile then Vernac.load_vernac false !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else try let inferedrc = List.find CUnix.file_readable_p [ - Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname^"."^Coq_config.version; - Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname; - Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname^"."^Coq_config.version; - Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname; - ] in - Vernac.load_vernac false inferedrc + else + try + let warn x = msg_warning (str x) in + let inferedrc = List.find CUnix.file_readable_p [ + Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; + Envars.xdg_config_home warn / rcdefaultname; + Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; + Envars.home ~warn / "."^rcdefaultname + ] in + Vernac.load_vernac false inferedrc with Not_found -> () (* Flags.if_verbose @@ -91,9 +94,9 @@ let theories_dirs_map = [ (* Initializes the LoadPath *) let init_load_path () = - let coqlib = Envars.coqlib Errors.error in + let coqlib = Envars.coqlib ~fail:Errors.error in let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in + let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in let coqpath = Envars.coqpath in let dirs = ["plugins"] in (* NOTE: These directories are searched from last to first *) @@ -129,7 +132,7 @@ let init_ocaml_path () = let add_subdir dl = Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) in - Mltop.add_ml_dir (Envars.coqlib Errors.error); + Mltop.add_ml_dir (Envars.coqlib ~fail:Errors.error); List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ecd9cafac..b104ef4c8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -23,7 +23,7 @@ let fatal_error info = let get_version_date () = try - let coqlib = Envars.coqlib Errors.error in + let coqlib = Envars.coqlib ~fail:Errors.error in let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in @@ -295,7 +295,9 @@ let parse_args arglist = | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem | "-coqlib" :: [] -> usage () - | "-where" :: _ -> print_endline (Envars.coqlib Errors.error); exit (if !filter_opts then 2 else 0) + | "-where" :: _ -> + print_endline (Envars.coqlib ~fail:Errors.error); + exit (if !filter_opts then 2 else 0) | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8e1864461..1bfc8f701 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -94,7 +94,7 @@ let print_usage_coqc () = let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" (Envars.coqlib Errors.error); + Printf.printf "COQLIB=%s/\n" (Envars.coqlib ~fail:Errors.error); Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; |