diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-31 09:09:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 17:20:35 +0100 |
| commit | 5268efdefb396267bfda0c17eb045fa2ed516b3c (patch) | |
| tree | b27a12e165d2c5b8c1b4d3171f961b8a5025bbb3 /toplevel | |
| parent | e03513b7309008a45957609739bcdaf3789f3052 (diff) | |
Using same code for browsing physical directories in coqtop and coqdep.
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0b9bb2f2e..ffdd84619 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -455,7 +455,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> exclude_search_in_dirname (next ()) + |"-exclude-dir" -> Systemdirs.exclude_directory (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 357c5482f..ef2e62c3b 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -11,6 +11,7 @@ open Util open Pp open Flags open Libobject +open Systemdirs open System (* Code to hook Coq into the ML toplevel -- depends on having the @@ -155,7 +156,7 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path *) +(* For Rec Add ML Path (-R) *) let add_rec_ml_dir unix_path = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) |