diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/cMap.ml | 42 | ||||
-rw-r--r-- | lib/cMap.mli | 15 | ||||
-rw-r--r-- | lib/envars.ml | 27 | ||||
-rw-r--r-- | lib/envars.mli | 13 | ||||
-rw-r--r-- | lib/feedback.ml | 6 | ||||
-rw-r--r-- | lib/feedback.mli | 2 | ||||
-rw-r--r-- | lib/flags.ml | 6 | ||||
-rw-r--r-- | lib/flags.mli | 4 | ||||
-rw-r--r-- | lib/hMap.ml | 14 | ||||
-rw-r--r-- | lib/pp.ml | 6 | ||||
-rw-r--r-- | lib/pp.mli | 4 | ||||
-rw-r--r-- | lib/richpp.ml | 34 | ||||
-rw-r--r-- | lib/richpp.mli | 26 | ||||
-rw-r--r-- | lib/serialize.ml | 4 | ||||
-rw-r--r-- | lib/serialize.mli | 2 | ||||
-rw-r--r-- | lib/system.ml | 95 | ||||
-rw-r--r-- | lib/system.mli | 38 |
17 files changed, 262 insertions, 76 deletions
diff --git a/lib/cMap.ml b/lib/cMap.ml index cf590d96c..876f84736 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 23d3801e0..cd3d2f5b1 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/envars.ml b/lib/envars.ml index b0eed8386..bafe2401b 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -143,23 +143,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} *) @@ -170,9 +159,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 @@ -180,7 +167,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 b62b9f28a..7c20c035a 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 a5e16ea04..1726da2fd 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 52a0e9fe6..38c867f5b 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 ab4ac03f8..9a0d4b5ec 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 8e3713656..29a0bbef0 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/hMap.ml b/lib/hMap.ml index f902eded0..8e900cd58 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 @@ -412,7 +412,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 +511,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 3b1123a9d..d034e6761 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 c4a9c39d5..fff989ce0 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 a0d3c374b..7e4b58c9a 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 aa2e3f02a..b14bfb283 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 34d3e054c..f4eac5a6b 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 ddc56956c..7a62d5603 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -13,44 +13,85 @@ open Errors open Util open Unix -(* All subdirectories, recursively *) +(** Dealing with directories *) -let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_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 let _ = closedir (opendir dir) in true with Unix_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 (stat path).st_kind with Unix_error _ -> S_BLK with + | S_DIR -> f (FileDir (path,name)) + | S_REG -> f (FileRegular name) + | _ -> () + +let process_directory f path = + let dirh = opendir path in + try while true do apply_subdir f path (readdir dirh) done + with End_of_file -> 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 = - let dirh = opendir dir in - try - while true do - let f = readdir dirh in - if ok_dirname f then - let file = Filename.concat dir f in - try - begin match (stat file).st_kind with - | S_DIR -> - let newrel = rel @ [f] in - add file newrel; - traverse file newrel - | _ -> () - end - with Unix_error (e,s1,s2) -> () - done - with End_of_file -> - closedir dirh + 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 let rec search paths test = diff --git a/lib/system.mli b/lib/system.mli index 247d528b9..2e773fe96 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 |