diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-17 12:28:46 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-10 14:05:54 +0200 |
commit | 7c36b13fdc6412450de6face4df18aea9d9bbaac (patch) | |
tree | 8975af385eea59e829c1c04d11e95d20ab81fd0f /lib | |
parent | 3a3ec7e1f306a49008edf47476ea5fb410233b95 (diff) |
Restoring test on ident validity while browsing directory structure.
The test was abandoned at the time of merging subdirectory browsing
between coqdep and coqtop, and to limit at the same time the
dependency of coqdep in files such as unicode.cmo.
But checking ident validity speeds up browsing in arbitrary directory
structure and we restore it for this reason.
(One could also say that browsing arbitrary directory structures is
not intended, but in practice this may happen, as e.g. reported in
BZ#5734.)
Diffstat (limited to 'lib')
-rw-r--r-- | lib/minisys.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/lib/minisys.ml b/lib/minisys.ml index 706f0430c..389b18ad4 100644 --- a/lib/minisys.ml +++ b/lib/minisys.ml @@ -36,10 +36,15 @@ let skipped_dirnames = ref ["CVS"; "_darcs"] let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames +(* Note: this test is possibly used for Coq module/file names but also for + OCaml filenames, whose syntax as of today is more restrictive for + module names (only initial letter then letter, digits, _ or quote), + but more permissive (though disadvised) for file names *) + let ok_dirname f = not (f = "") && f.[0] != '.' && - not (List.mem f !skipped_dirnames) (*&& - (match Unicode.ident_refutation f with None -> true | _ -> false)*) + not (List.mem f !skipped_dirnames) && + match Unicode.ident_refutation f with None -> true | _ -> false (* Check directory can be opened *) @@ -55,10 +60,11 @@ let exists_dir dir = let apply_subdir f path name = (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) (* as well as skipped files like CVS, ... *) - if ok_dirname name then + let base = try Filename.chop_extension name with Invalid_argument _ -> name in + if ok_dirname base then let path = if path = "." then name else path//name in match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with - | Unix.S_DIR -> f (FileDir (path,name)) + | Unix.S_DIR when name = base -> f (FileDir (path,name)) | Unix.S_REG -> f (FileRegular name) | _ -> () |