diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e100025dd..278e87418 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -807,37 +807,34 @@ let vernac_set_used_variables l = (*****************************) (* Auxiliary file management *) +let expand filename = + Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename + let vernac_require_from export filename = - Library.require_library_from_file None - (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename) - export + Library.require_library_from_file None (expand filename) export let vernac_add_loadpath isrec pdir ldiropt = - let pdir = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) pdir in - let alias = match ldiropt with - | None -> Nameops.default_root_prefix - | Some ldir -> ldir in - (if isrec then Mltop.add_rec_path else Mltop.add_path) ~unix_path:pdir ~coq_root:alias + let pdir = expand pdir in + let alias = Option.default Nameops.default_root_prefix ldiropt in + (if isrec then Mltop.add_rec_path else Mltop.add_path) + ~unix_path:pdir ~coq_root:alias let vernac_remove_loadpath path = - Library.remove_load_path (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) + Library.remove_load_path (expand path) (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) - (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) + (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) let vernac_declare_ml_module local l = - Mltop.declare_ml_modules local (List.map - (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x))) - l) + Mltop.declare_ml_modules local (List.map expand l) let vernac_chdir = function | None -> msg_notice (str (Sys.getcwd())) | Some path -> begin - try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) + try Sys.chdir (expand path) with Sys_error err -> msg_warning (str ("Cd failed: " ^ err)) end; if_verbose msg_info (str (Sys.getcwd())) |