aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cMap.ml42
-rw-r--r--lib/cMap.mli15
-rw-r--r--lib/cSig.mli4
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/dyn.ml46
-rw-r--r--lib/dyn.mli16
-rw-r--r--lib/envars.ml27
-rw-r--r--lib/envars.mli13
-rw-r--r--lib/feedback.ml6
-rw-r--r--lib/feedback.mli2
-rw-r--r--lib/flags.ml6
-rw-r--r--lib/flags.mli4
-rw-r--r--lib/future.ml7
-rw-r--r--lib/future.mli3
-rw-r--r--lib/hMap.ml14
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/pp.ml33
-rw-r--r--lib/pp.mli4
-rw-r--r--lib/richpp.ml34
-rw-r--r--lib/richpp.mli26
-rw-r--r--lib/serialize.ml4
-rw-r--r--lib/serialize.mli2
-rw-r--r--lib/system.ml86
-rw-r--r--lib/system.mli38
-rw-r--r--lib/util.ml1
-rw-r--r--lib/util.mli2
26 files changed, 323 insertions, 114 deletions
diff --git a/lib/cMap.ml b/lib/cMap.ml
index cf590d96c3..876f847365 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -12,6 +12,13 @@ sig
val compare : t -> t -> int
end
+module type MonadS =
+sig
+ type +'a t
+ val return : 'a -> 'a t
+ val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
module type S = Map.S
module type ExtS =
@@ -30,6 +37,12 @@ sig
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
end
+ module Monad(M : MonadS) :
+ sig
+ val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ end
end
module MapExt (M : Map.OrderedType) :
@@ -47,6 +60,12 @@ sig
sig
val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
end
+ module Monad(MS : MonadS) :
+ sig
+ val fold : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+ val fold_left : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+ val fold_right : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+ end
end =
struct
(** This unsafe module is a way to access to the actual implementations of
@@ -159,6 +178,29 @@ struct
end
+ module Monad(M : MonadS) =
+ struct
+
+ open M
+
+ let rec fold_left f s accu = match map_prj s with
+ | MEmpty -> return accu
+ | MNode (l, k, v, r, h) ->
+ fold_left f l accu >>= fun accu ->
+ f k v accu >>= fun accu ->
+ fold_left f r accu
+
+ let rec fold_right f s accu = match map_prj s with
+ | MEmpty -> return accu
+ | MNode (l, k, v, r, h) ->
+ fold_right f r accu >>= fun accu ->
+ f k v accu >>= fun accu ->
+ fold_right f l accu
+
+ let fold = fold_left
+
+ end
+
end
module Make(M : Map.OrderedType) =
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 23d3801e08..cd3d2f5b19 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -14,6 +14,13 @@ sig
val compare : t -> t -> int
end
+module type MonadS =
+sig
+ type +'a t
+ val return : 'a -> 'a t
+ val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
module type S = Map.S
module type ExtS =
@@ -59,6 +66,14 @@ sig
i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *)
end
+ module Monad(M : MonadS) :
+ sig
+ val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ end
+ (** Fold operators parameterized by any monad. *)
+
end
module Make(M : Map.OrderedType) : ExtS with
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 2a8bda2936..796e58cbfb 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b
type 'a until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
+type (_, _) eq = Refl : ('a, 'a) eq
+
module type SetS =
sig
type elt
@@ -45,3 +47,5 @@ sig
end
(** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
documentation for more information. *)
+
+module type EmptyS = sig end
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 7ff1d29359..1770df1993 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -8,6 +8,7 @@ Hashcons
CSet
CMap
Int
+Dyn
HMap
Option
Store
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 056b687313..826cfaf8db 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,12 +6,24 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
-open Pp
-
+module type S =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
+
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
+val dump : unit -> (int * string) list
+end
+
+module Make(M : CSig.EmptyS) =
+struct
(* Dynamics, programmed with DANGER !!! *)
-type t = int * Obj.t
+type 'a tag = int
+
+type t = Dyn : 'a tag * 'a -> t
let dyntab = ref (Int.Map.empty : string Int.Map.t)
(** Instead of working with tags as strings, which are costly, we use their
@@ -24,27 +36,21 @@ let create (s : string) =
let () =
if Int.Map.mem hash !dyntab then
let old = Int.Map.find hash !dyntab in
- let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in
- anomaly ~label:"Dyn.create" msg
+ let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+ assert false
in
let () = dyntab := Int.Map.add hash s !dyntab in
- let infun v = (hash, Obj.repr v) in
- let outfun (nh, rv) =
- if Int.equal hash nh then Obj.magic rv
- else
- anomaly (str "dyn_out: expected " ++ str s)
- in
- (infun, outfun)
+ hash
-let has_tag (s, _) tag =
- let hash = Hashtbl.hash (tag : string) in
- Int.equal s hash
+let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
+ fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
-let tag (s,_) =
+let repr s =
try Int.Map.find s !dyntab
with Not_found ->
- anomaly (str "Unknown dynamic tag " ++ int s)
-
-let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
+ let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
+ assert false
let dump () = Int.Map.bindings !dyntab
+
+end \ No newline at end of file
diff --git a/lib/dyn.mli b/lib/dyn.mli
index cac912aca1..28587859e1 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -8,10 +8,16 @@
(** Dynamics. Use with extreme care. Not for kids. *)
-type t
+module type S =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
-val create : string -> ('a -> t) * (t -> 'a)
-val tag : t -> string
-val has_tag : t -> string -> bool
-val pointer_equal : t -> t -> bool
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
val dump : unit -> (int * string) list
+end
+
+(** FIXME: use OCaml 4.02 generative functors when available *)
+module Make(M : CSig.EmptyS) : S
diff --git a/lib/envars.ml b/lib/envars.ml
index 2b8af917fa..512114d5dc 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,23 +146,12 @@ let coqpath =
let exe s = s ^ Coq_config.exec_extension
-let guess_camlbin () = which (user_path ()) (exe "ocamlc")
+let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
-let camlbin () =
- if !Flags.camlbin_spec then !Flags.camlbin else
- if !Flags.boot then Coq_config.camlbin else
- try guess_camlbin () with Not_found -> Coq_config.camlbin
-
-let ocamlc () = camlbin () / Coq_config.ocamlc
-
-let ocamlopt () = camlbin () / Coq_config.ocamlopt
-
-let camllib () =
- if !Flags.boot then
- Coq_config.camllib
- else
- let _, res = CUnix.run_command (ocamlc () ^ " -where") in
- String.strip res
+let ocamlfind () =
+ if !Flags.ocamlfind_spec then !Flags.ocamlfind else
+ if !Flags.boot then Coq_config.ocamlfind else
+ try guess_ocamlfind () / "ocamlfind" with Not_found -> Coq_config.ocamlfind
(** {2 Camlp4 paths} *)
@@ -173,9 +162,7 @@ let camlp4bin () =
if !Flags.boot then Coq_config.camlp4bin else
try guess_camlp4bin ()
with Not_found ->
- let cb = camlbin () in
- if Sys.file_exists (cb / exe Coq_config.camlp4) then cb
- else Coq_config.camlp4bin
+ Coq_config.camlp4bin
let camlp4 () = camlp4bin () / exe Coq_config.camlp4
@@ -183,7 +170,7 @@ let camlp4lib () =
if !Flags.boot then
Coq_config.camlp4lib
else
- let ex, res = CUnix.run_command (camlp4 () ^ " -where") in
+ let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in
match ex with
| Unix.WEXITED 0 -> String.strip res
| _ -> "/dev/null"
diff --git a/lib/envars.mli b/lib/envars.mli
index b62b9f28a9..7c20c035a5 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -47,17 +47,8 @@ val coqroot : string
the order it gets added to the search path. *)
val coqpath : string list
-(** [camlbin ()] is the path to the ocaml binaries. *)
-val camlbin : unit -> string
-
-(** [camllib ()] is the path to the ocaml standard library. *)
-val camllib : unit -> string
-
-(** [ocamlc ()] is the ocaml bytecode compiler that compiled this Coq. *)
-val ocamlc : unit -> string
-
-(** [ocamlc ()] is the ocaml native compiler that compiled this Coq. *)
-val ocamlopt : unit -> string
+(** [camlbin ()] is the path to the ocamlfind binary. *)
+val ocamlfind : unit -> string
(** [camlp4bin ()] is the path to the camlp4 binary. *)
val camlp4bin : unit -> string
diff --git a/lib/feedback.ml b/lib/feedback.ml
index a5e16ea04c..1726da2fdb 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -18,7 +18,7 @@ type message_level =
type message = {
message_level : message_level;
- message_content : string;
+ message_content : xml;
}
let of_message_level = function
@@ -39,12 +39,12 @@ let to_message_level =
let of_message msg =
let lvl = of_message_level msg.message_level in
- let content = Serialize.of_string msg.message_content in
+ let content = Serialize.of_xml msg.message_content in
Xml_datatype.Element ("message", [], [lvl; content])
let to_message xml = match xml with
| Xml_datatype.Element ("message", [], [lvl; content]) -> {
message_level = to_message_level lvl;
- message_content = Serialize.to_string content }
+ message_content = Serialize.to_xml content }
| _ -> raise Serialize.Marshal_error
let is_message = function
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 52a0e9fe6f..38c867f5b5 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -18,7 +18,7 @@ type message_level =
type message = {
message_level : message_level;
- message_content : string;
+ message_content : xml;
}
val of_message : message -> xml
diff --git a/lib/flags.ml b/lib/flags.ml
index ab4ac03f80..9a0d4b5ec1 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -193,9 +193,9 @@ let is_standard_doc_url url =
let coqlib_spec = ref false
let coqlib = ref "(not initialized yet)"
-(* Options for changing camlbin (used by coqmktop) *)
-let camlbin_spec = ref false
-let camlbin = ref Coq_config.camlbin
+(* Options for changing ocamlfind (used by coqmktop) *)
+let ocamlfind_spec = ref false
+let ocamlfind = ref Coq_config.camlbin
(* Options for changing camlp4bin (used by coqmktop) *)
let camlp4bin_spec = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 8e37136560..29a0bbef01 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -120,8 +120,8 @@ val coqlib_spec : bool ref
val coqlib : string ref
(** Options for specifying where OCaml binaries reside *)
-val camlbin_spec : bool ref
-val camlbin : string ref
+val ocamlfind_spec : bool ref
+val ocamlfind : string ref
val camlp4bin_spec : bool ref
val camlp4bin : string ref
diff --git a/lib/future.ml b/lib/future.ml
index 78a158264b..b6012ed207 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -7,8 +7,9 @@
(************************************************************************)
(* To deal with side effects we have to save/restore the system state *)
-let freeze = ref (fun () -> assert false : unit -> Dyn.t)
-let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
+type freeze
+let freeze = ref (fun () -> assert false : unit -> freeze)
+let unfreeze = ref (fun _ -> () : freeze -> unit)
let set_freeze f g = freeze := f; unfreeze := g
let not_ready_msg = ref (fun name ->
@@ -58,7 +59,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
and 'a comp =
| Delegated of (unit -> unit)
| Closure of (unit -> 'a)
- | Val of 'a * Dyn.t option
+ | Val of 'a * freeze option
| Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *)
and 'a comput =
diff --git a/lib/future.mli b/lib/future.mli
index adc15e49c7..29b71b70a8 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -157,10 +157,11 @@ val transactify : ('a -> 'b) -> 'a -> 'b
(** Debug: print a computation given an inner printing function. *)
val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
+type freeze
(* These functions are needed to get rid of side effects.
Thy are set for the outermos layer of the system, since they have to
deal with the whole system state. *)
-val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit
val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
diff --git a/lib/hMap.ml b/lib/hMap.ml
index f902eded03..8e900cd581 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -329,4 +329,18 @@ struct
Int.Map.map fs s
end
+ module Monad(M : CMap.MonadS) =
+ struct
+ module IntM = Int.Map.Monad(M)
+ module ExtM = Map.Monad(M)
+ open M
+
+ let fold f s accu =
+ let ff _ m accu = ExtM.fold f m accu in
+ IntM.fold ff s accu
+
+ let fold_left _ _ _ = assert false
+ let fold_right _ _ _ = assert false
+ end
+
end
diff --git a/lib/lib.mllib b/lib/lib.mllib
index f3f6ad8fc7..a9181c51c1 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
Errors
Bigint
-Dyn
Segmenttree
Unicodetable
Unicode
diff --git a/lib/pp.ml b/lib/pp.ml
index 4ed4b17791..a1913c98f7 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -51,25 +51,18 @@ sig
val prj : t -> 'a key -> 'a option
end =
struct
- (** See module {Dyn} for more details. *)
- type t = int * Obj.t
+module Dyn = Dyn.Make(struct end)
- type 'a key = int
-
- let dyntab = ref (Int.Map.empty : string Int.Map.t)
-
- let create (s : string) =
- let hash = Hashtbl.hash s in
- let () = assert (not (Int.Map.mem hash !dyntab)) in
- let () = dyntab := Int.Map.add hash s !dyntab in
- hash
-
- let inj x h = (h, Obj.repr x)
-
- let prj (nh, rv) h =
- if Int.equal h nh then Some (Obj.magic rv)
- else None
+type t = Dyn.t
+type 'a key = 'a Dyn.tag
+let create = Dyn.create
+let inj x k = Dyn.Dyn (k, x)
+let prj : type a. t -> a key -> a option = fun dyn k ->
+ let Dyn.Dyn (k', x) = dyn in
+ match Dyn.eq k k' with
+ | None -> None
+ | Some CSig.Refl -> Some x
end
@@ -412,7 +405,7 @@ type message_level = Feedback.message_level =
type message = Feedback.message = {
message_level : message_level;
- message_content : string;
+ message_content : Xml_datatype.xml;
}
let of_message = Feedback.of_message
@@ -511,11 +504,11 @@ let string_of_ppcmds c =
msg_with Format.str_formatter c;
Format.flush_str_formatter ()
-let log_via_feedback () = logger := (fun ~id lvl msg ->
+let log_via_feedback printer = logger := (fun ~id lvl msg ->
!feeder {
Feedback.contents = Feedback.Message {
message_level = lvl;
- message_content = string_of_ppcmds msg };
+ message_content = printer msg };
Feedback.route = !feedback_route;
Feedback.id = id })
diff --git a/lib/pp.mli b/lib/pp.mli
index 3b1123a9dc..d034e67617 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -116,7 +116,7 @@ type message_level = Feedback.message_level =
type message = Feedback.message = {
message_level : message_level;
- message_content : string;
+ message_content : Xml_datatype.xml;
}
type logger = message_level -> std_ppcmds -> unit
@@ -154,7 +154,7 @@ val std_logger : logger
val set_logger : logger -> unit
-val log_via_feedback : unit -> unit
+val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit
val of_message : message -> Xml_datatype.xml
val to_message : Xml_datatype.xml -> message
diff --git a/lib/richpp.ml b/lib/richpp.ml
index c4a9c39d5a..fff989ce0a 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -163,4 +163,38 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
in
node xml
+type richpp = xml
+let repr xml = xml
+let richpp_of_xml xml = xml
+let richpp_of_string s = PCData s
+
+let richpp_of_pp pp =
+ let annotate t = match Pp.Tag.prj t Ppstyle.tag with
+ | None -> None
+ | Some key -> Some (Ppstyle.repr key)
+ in
+ let rec drop = function
+ | PCData s -> [PCData s]
+ | Element (_, annotation, cs) ->
+ let cs = List.concat (List.map drop cs) in
+ match annotation.annotation with
+ | None -> cs
+ | Some s -> [Element (String.concat "." s, [], cs)]
+ in
+ let xml = rich_pp annotate pp in
+ Element ("_", [], drop xml)
+
+let raw_print xml =
+ let buf = Buffer.create 1024 in
+ let rec print = function
+ | PCData s -> Buffer.add_string buf s
+ | Element (_, _, cs) -> List.iter print cs
+ in
+ let () = print xml in
+ Buffer.contents buf
+
+let of_richpp x = Element ("richpp", [], [x])
+let to_richpp xml = match xml with
+| Element ("richpp", [], [x]) -> x
+| _ -> raise Serialize.Marshal_error
diff --git a/lib/richpp.mli b/lib/richpp.mli
index a0d3c374b2..7e4b58c9a6 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -39,3 +39,29 @@ val xml_of_rich_pp :
('annotation -> (string * string) list) ->
'annotation located Xml_datatype.gxml ->
Xml_datatype.xml
+
+(** {5 Enriched text} *)
+
+type richpp
+(** Type of text with style annotations *)
+
+val richpp_of_pp : Pp.std_ppcmds -> richpp
+(** Extract style information from formatted text *)
+
+val richpp_of_xml : Xml_datatype.xml -> richpp
+(** Do not use outside of dedicated areas *)
+
+val richpp_of_string : string -> richpp
+(** Make a styled text out of a normal string *)
+
+val repr : richpp -> Xml_datatype.xml
+(** Observe the styled text as XML *)
+
+(** {5 Serialization} *)
+
+val of_richpp : richpp -> Xml_datatype.xml
+val to_richpp : Xml_datatype.xml -> richpp
+
+(** Represent the semi-structured document as a string, dropping any additional
+ information. *)
+val raw_print : richpp -> string
diff --git a/lib/serialize.ml b/lib/serialize.ml
index aa2e3f02a4..b14bfb2833 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -114,3 +114,7 @@ let to_loc xml =
with Not_found | Invalid_argument _ -> raise Marshal_error)
| _ -> raise Marshal_error
+let of_xml x = Element ("xml", [], [x])
+let to_xml xml = match xml with
+| Element ("xml", [], [x]) -> x
+| _ -> raise Marshal_error
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 34d3e054cd..f4eac5a6b9 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -35,3 +35,5 @@ val of_edit_id: int -> xml
val to_edit_id: xml -> int
val of_loc : Loc.t -> xml
val to_loc : xml -> Loc.t
+val of_xml : xml -> xml
+val to_xml : xml -> xml
diff --git a/lib/system.ml b/lib/system.ml
index a902229609..b57c02a14f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,35 +12,85 @@ open Pp
open Errors
open Util
-(* All subdirectories, recursively *)
+(** Dealing with directories *)
-let exists_dir dir =
- try Sys.is_directory dir with Sys_error _ -> false
+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_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
+let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
let ok_dirname f =
- not (String.is_empty f) && f.[0] != '.' &&
- not (String.List.mem f !skipped_dirnames) &&
- (match Unicode.ident_refutation f with None -> true | _ -> false)
+ 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 name.[0] <> '.' && 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 process_directory f path =
+ let dirh = Unix.opendir path in
+ try while true do apply_subdir f path (Unix.readdir dirh) done
+ with End_of_file -> Unix.closedir dirh
+
+let process_subdirectories f path =
+ let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+ process_directory f path
+
+(** Returns the list of all recursive subdirectories of [root] in
+ depth-first search, with sons ordered as on the file system;
+ warns if [root] does not exist *)
let all_subdirs ~unix_path:root =
let l = ref [] in
let add f rel = l := (f, rel) :: !l in
- let rec traverse dir rel =
- Array.iter (fun f ->
- if ok_dirname f then
- let file = Filename.concat dir f in
- if Sys.is_directory file then begin
- let newrel = rel @ [f] in
- add file newrel;
- traverse file newrel
- end)
- (Sys.readdir dir)
+ let rec traverse path rel =
+ let f = function
+ | FileDir (path,f) ->
+ let newrel = rel @ [f] in
+ add path newrel;
+ traverse path newrel
+ | _ -> ()
+ in process_directory f path
in
- if exists_dir root then traverse root [];
+ check_unix_dir (fun s -> msg_warning (str s)) root;
+ if exists_dir root then traverse root []
+ else msg_warning (str ("Cannot open " ^ root));
List.rev !l
(* Caching directory contents for efficient syntactic equality of file
diff --git a/lib/system.mli b/lib/system.mli
index c2d64fe0d0..7a91e005c6 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,14 +8,46 @@
(** {5 Coqtop specific system utilities} *)
+(** {6 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 *)
+
+val (//) : unix_path -> string -> unix_path
+
+val exists_dir : unix_path -> bool
+
+(** [check_unix_dir warn path] calls [warn] with an appropriate
+ message if [path] looks does not look like a Unix path on Windows *)
+
+val check_unix_dir : (string -> unit) -> unix_path -> unit
+
+(** [exclude_search_in_dirname path] excludes [path] when processing
+ directories *)
+
+val exclude_directory : unix_path -> unit
+
+(** [process_directory f path] applies [f] on contents of directory
+ [path]; fails with Unix_error if the latter does not exists; skips
+ all files or dirs starting with "." *)
+
+val process_directory : (file_kind -> unit) -> unix_path -> unit
+
+(** [process_subdirectories f path] applies [f path/file file] on each
+ [file] of the directory [path]; fails with Unix_error if the
+ latter does not exists; kips all files or dirs starting with "." *)
+
+val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
+
(** {6 Files and load paths} *)
(** Load path entries remember the original root
given by the user. For efficiency, we keep the full path (field
[directory]), the root path and the path relative to the root. *)
-val exclude_search_in_dirname : string -> unit
-
val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
val is_in_path : CUnix.load_path -> string -> bool
val is_in_system_path : string -> bool
@@ -24,8 +56,6 @@ val where_in_path :
val where_in_path_rex :
CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
-val exists_dir : string -> bool
-
val find_file_in_path :
?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
diff --git a/lib/util.ml b/lib/util.ml
index a20dba0fc4..b67539918d 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -124,6 +124,7 @@ let delayed_force f = f ()
type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
let map_union f g = function
| Inl a -> Inl (f a)
diff --git a/lib/util.mli b/lib/util.mli
index 1dc405fcbe..0ce6cc6603 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -111,5 +111,7 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
val open_utf8_file_in : string -> in_channel
(** Open an utf-8 encoded file and skip the byte-order mark if any. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 17:01:39 +0000