aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-01 00:59:46 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-01 00:59:46 +0200
commit114d5f0d0bca9f01d7a5ab3381a9b9ca4291191a (patch)
tree3aeacfad3a11279599bf4362f8318eb2d8b62ccd /lib
parent842dfef1d52c739119808ea1dec3509c0cf86435 (diff)
parentd0a9edabf59a858625d11516cdb230d223a77aeb (diff)
Merge branch 'yet-another-makefile-bigbang' into trunk
Diffstat (limited to 'lib')
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/minisys.ml74
-rw-r--r--lib/system.ml60
3 files changed, 76 insertions, 59 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 2be435f6f..a6c09058d 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -3,6 +3,7 @@ Bigint
Segmenttree
Unicodetable
Unicode
+Minisys
System
CThread
Spawn
diff --git a/lib/minisys.ml b/lib/minisys.ml
new file mode 100644
index 000000000..25e4d79c4
--- /dev/null
+++ b/lib/minisys.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Minisys regroups some code that used to be in System.
+ Unlike System, this module has no dependency and could
+ be used for initial compilation target such as coqdep_boot.
+ The functions here are still available in System thanks to
+ an include. For the signature, look at the top of system.mli
+*)
+
+(** Dealing with directories *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+ | FileDir of unix_path * (* basename of path: *) string
+ | FileRegular of string (* basename of file *)
+
+(* Copy of Filename.concat but assuming paths to always be POSIX *)
+
+let (//) dirname filename =
+ let l = String.length dirname in
+ if l = 0 || dirname.[l-1] = '/'
+ then dirname ^ filename
+ else dirname ^ "/" ^ filename
+
+(* Excluding directories; We avoid directories starting with . as well
+ as CVS and _darcs and any subdirs given via -exclude-dir *)
+
+let skipped_dirnames = ref ["CVS"; "_darcs"]
+
+let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
+
+let ok_dirname f =
+ not (f = "") && f.[0] != '.' &&
+ not (List.mem f !skipped_dirnames) (*&&
+ (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+
+(* Check directory can be opened *)
+
+let exists_dir dir =
+ try Sys.is_directory dir with Sys_error _ -> false
+
+let check_unix_dir warn dir =
+ if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
+ (String.length dir > 2 && dir.[1] = ':' ||
+ String.contains dir '\\' ||
+ String.contains dir ';')
+ then warn ("assuming " ^ dir ^
+ " to be a Unix path even if looking like a Win32 path.")
+
+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 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_REG -> f (FileRegular name)
+ | _ -> ()
+
+let readdir dir = try Sys.readdir dir with any -> [||]
+
+let process_directory f path =
+ Array.iter (apply_subdir f path) (readdir path)
+
+let process_subdirectories f path =
+ let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+ process_directory f path
diff --git a/lib/system.ml b/lib/system.ml
index 8cdcaf5dc..8b53a11d6 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,65 +12,7 @@ open Pp
open Errors
open Util
-(** Dealing with directories *)
-
-type unix_path = string (* path in unix-style, with '/' separator *)
-
-type file_kind =
- | FileDir of unix_path * (* basename of path: *) string
- | FileRegular of string (* basename of file *)
-
-(* Copy of Filename.concat but assuming paths to always be POSIX *)
-
-let (//) dirname filename =
- let l = String.length dirname in
- if l = 0 || dirname.[l-1] = '/'
- then dirname ^ filename
- else dirname ^ "/" ^ filename
-
-(* Excluding directories; We avoid directories starting with . as well
- as CVS and _darcs and any subdirs given via -exclude-dir *)
-
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
- not (f = "") && f.[0] != '.' &&
- not (List.mem f !skipped_dirnames) (*&&
- (match Unicode.ident_refutation f with None -> true | _ -> false)*)
-
-(* Check directory can be opened *)
-
-let exists_dir dir =
- try Sys.is_directory dir with Sys_error _ -> false
-
-let check_unix_dir warn dir =
- if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
- (String.length dir > 2 && dir.[1] = ':' ||
- String.contains dir '\\' ||
- String.contains dir ';')
- then warn ("assuming " ^ dir ^
- " to be a Unix path even if looking like a Win32 path.")
-
-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 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_REG -> f (FileRegular name)
- | _ -> ()
-
-let readdir dir = try Sys.readdir dir with any -> [||]
-
-let process_directory f path =
- Array.iter (apply_subdir f path) (readdir path)
-
-let process_subdirectories f path =
- let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
- process_directory f path
+include Minisys
(** Returns the list of all recursive subdirectories of [root] in
depth-first search, with sons ordered as on the file system;