Merge PR #1054: Restoring test on ident validity while browsing directory structure.

3 files changed, 26 insertions, 4 deletions

diff --git a/lib/minisys.ml b/lib/minisys.ml
index 706f0430c3..389b18ad4e 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)
     | _ -> ()
 
diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml
index 9ce348a0bd..d0ded4cb59 100644
--- a/lib/segmenttree.ml
+++ b/lib/segmenttree.ml
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 (** This module is a very simple implementation of "segment trees".
 
     A segment tree of type ['a t] represents a mapping from a union of
diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli
index 3258537b99..e274a6fdc8 100644
--- a/lib/segmenttree.mli
+++ b/lib/segmenttree.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 (** This module is a very simple implementation of "segment trees".
 
     A segment tree of type ['a t] represents a mapping from a union of