From 3a3ec7e1f306a49008edf47476ea5fb410233b95 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Sep 2017 16:56:21 +0200
Subject: Adding headers to segmenttree.{ml,mli}.

---
 lib/segmenttree.ml  | 8 ++++++++
 lib/segmenttree.mli | 8 ++++++++
 2 files changed, 16 insertions(+)

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
-- 
cgit v1.2.3


From 7c36b13fdc6412450de6face4df18aea9d9bbaac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Sep 2017 12:28:46 +0200
Subject: 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.)
---
 Makefile.build | 16 ++++++++++------
 lib/minisys.ml | 14 ++++++++++----
 2 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 7b2e209a25..eb19f43e71 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -430,14 +430,18 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT)
 
 # Remember to update the dependencies below when you add files!
 
-COQDEPBOOTSRC := lib/minisys.cmo \
- lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \
+COQDEPBOOTSRC := \
+ lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \
  tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo
 
 lib/segmenttree.cmo : lib/segmenttree.cmi
 lib/segmenttree.cmx : lib/segmenttree.cmi
-lib/unicode.cmo : lib/unicodetable.cmo lib/segmenttree.cmi lib/unicode.cmi
-lib/unicode.cmx : lib/unicodetable.cmx lib/segmenttree.cmx lib/unicode.cmi
+lib/unicodetable.cmo : lib/segmenttree.cmo
+lib/unicodetable.cmx : lib/segmenttree.cmx
+lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi
+lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi
+lib/minisys.cmo : lib/unicode.cmo
+lib/minisys.cmx : lib/unicode.cmx
 tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi
 tools/coqdep_lexer.cmx : lib/unicode.cmx tools/coqdep_lexer.cmi
 tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi
@@ -455,8 +459,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 
 # The full coqdep (unused by this build, but distributed by make install)
 
-COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo lib/minisys.cmo \
-  lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \
+COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \
+  lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \
   lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \
   tools/coqdep.cmo
 
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)
     | _ -> ()
 
-- 
cgit v1.2.3