diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/mltop.ml4 | 5 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 20 |
3 files changed, 16 insertions, 10 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 4449137e8b..591b7b5a8d 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -42,9 +42,8 @@ open Vernacinterp (* This path is where we look for .cmo *) let coq_mlpath_copy = ref ["."] -let keep_copy_mlpath s = - let dir = glob s in - coq_mlpath_copy := dir :: !coq_mlpath_copy +let keep_copy_mlpath path = + coq_mlpath_copy := path :: !coq_mlpath_copy (* If there is a toplevel under Coq *) type toplevel = { diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 746a9a9f4d..185bfd93c8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -119,6 +119,7 @@ let pr_new_syntax loc ocom = let rec vernac_com interpfun (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> + let fname = expand_path_macros fname in (* translator state *) let ch = !chan_translate in let cs = Lexer.com_state() in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5ae3998f31..db30d7b950 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -597,28 +597,34 @@ let vernac_proof_instr instr = (* Auxiliary file management *) let vernac_require_from export spec filename = - Library.require_library_from_file None filename export + Library.require_library_from_file None + (System.expand_path_macros filename) + export let vernac_add_loadpath isrec pdir ldiropt = + let pdir = System.expand_path_macros 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) pdir alias -let vernac_remove_loadpath = Library.remove_load_path +let vernac_remove_loadpath path = + Library.remove_load_path (System.expand_path_macros path) (* Coq syntax for ML or system commands *) -let vernac_add_ml_path isrec s = - (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (System.glob s) +let vernac_add_ml_path isrec path = + (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) + (System.expand_path_macros path) -let vernac_declare_ml_module l = Mltop.declare_ml_modules l +let vernac_declare_ml_module l = + Mltop.declare_ml_modules (List.map System.expand_path_macros l) let vernac_chdir = function | None -> message (Sys.getcwd()) - | Some s -> + | Some path -> begin - try Sys.chdir (System.glob s) + try Sys.chdir (System.expand_path_macros path) with Sys_error str -> warning ("Cd failed: " ^ str) end; if_verbose message (Sys.getcwd()) |