aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/control.ml6
-rw-r--r--lib/coqProject_file.ml414
-rw-r--r--lib/flags.ml6
-rw-r--r--lib/flags.mli2
-rw-r--r--lib/minisys.ml6
-rw-r--r--lib/pp.ml40
-rw-r--r--lib/pp.mli5
-rw-r--r--lib/profile.ml29
-rw-r--r--lib/terminal.ml12
-rw-r--r--lib/terminal.mli5
10 files changed, 79 insertions, 46 deletions
diff --git a/lib/control.ml b/lib/control.ml
index d9b91be3a0..f5d7df204e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -48,7 +48,7 @@ let windows_timeout n f e =
let exited = ref false in
let thread init =
while not !killed do
- let cur = Unix.time () in
+ let cur = Unix.gettimeofday () in
if float_of_int n <= cur -. init then begin
interrupt := true;
exited := true;
@@ -57,12 +57,12 @@ let windows_timeout n f e =
Thread.delay 0.5
done
in
- let init = Unix.time () in
+ let init = Unix.gettimeofday () in
let _id = Thread.create thread init in
try
let res = f () in
let () = killed := true in
- let cur = Unix.time () in
+ let cur = Unix.gettimeofday () in
(** The thread did not interrupt, but the computation took longer than
expected. *)
let () = if float_of_int n <= cur -. init then begin
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index bb3cbabbd6..13de731f54 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -73,9 +73,6 @@ let rec post_canonize f =
if dir = Filename.current_dir_name then f else post_canonize dir
else f
-(* Avoid Sys.is_directory raise an exception (if the file does not exists) *)
-let is_directory f = Sys.file_exists f && Sys.is_directory f
-
(********************* parser *******************************************)
exception Parsing_error of string
@@ -106,6 +103,15 @@ let parse f =
res
;;
+(* Copy from minisys.ml, since we don't see that file here *)
+let exists_dir dir =
+ let rec strip_trailing_slash dir =
+ let len = String.length dir in
+ if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
+ then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
+ try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
+
+
let process_cmd_line orig_dir proj args =
let orig_dir = (* avoids turning foo.v in ./foo.v *)
if orig_dir = "." then "" else orig_dir in
@@ -173,7 +179,7 @@ let process_cmd_line orig_dir proj args =
| f :: r ->
let f = CUnix.correct_path f orig_dir in
let proj =
- if is_directory f then { proj with subdirs = proj.subdirs @ [f] }
+ if exists_dir f then { proj with subdirs = proj.subdirs @ [f] }
else match CUnix.get_extension f with
| ".v" -> { proj with v_files = proj.v_files @ [f] }
| ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
diff --git a/lib/flags.ml b/lib/flags.ml
index 5d9d9dcf50..0bce22f584 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,7 +106,7 @@ let we_are_parsing = ref false
(* Current means no particular compatibility consideration.
For correct comparisons, this constructor should remain the last one. *)
-type compat_version = VOld | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current
let compat_version = ref Current
@@ -120,6 +120,9 @@ let version_compare v1 v2 = match v1, v2 with
| V8_6, V8_6 -> 0
| V8_6, _ -> -1
| _, V8_6 -> 1
+ | V8_7, V8_7 -> 0
+ | V8_7, _ -> -1
+ | _, V8_7 -> 1
| Current, Current -> 0
let version_strictly_greater v = version_compare !compat_version v > 0
@@ -129,6 +132,7 @@ let pr_version = function
| VOld -> "old"
| V8_5 -> "8.5"
| V8_6 -> "8.6"
+ | V8_7 -> "8.7"
| Current -> "current"
(* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index e63f1ec26d..eb4c37a548 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -77,7 +77,7 @@ val raw_print : bool ref
(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
val univ_print : bool ref
-type compat_version = VOld | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current
val compat_version : compat_version ref
val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
diff --git a/lib/minisys.ml b/lib/minisys.ml
index b4382a3fe7..1ed017e489 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -44,7 +44,11 @@ let ok_dirname f =
(* Check directory can be opened *)
let exists_dir dir =
- try Sys.is_directory dir with Sys_error _ -> false
+ let rec strip_trailing_slash dir =
+ let len = String.length dir in
+ if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
+ then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
+ try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
let apply_subdir f path name =
(* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
diff --git a/lib/pp.ml b/lib/pp.ml
index 6d28ed13b9..eccaa09288 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -153,7 +153,7 @@ let rec pr_com ft s =
| None -> ()
(* pretty printing functions *)
-let pp_with ft =
+let pp_with ft pp =
let cpp_open_box = function
| Pp_hbox n -> Format.pp_open_hbox ft ()
| Pp_vbox n -> Format.pp_open_vbox ft n
@@ -175,7 +175,7 @@ let pp_with ft =
pp_cmd s;
pp_close_tag ft ()
in
- try pp_cmd
+ try pp_cmd pp
with reraise ->
let reraise = Backtrace.add_backtrace reraise in
let () = Format.pp_print_flush ft () in
@@ -220,23 +220,25 @@ let prlist pr l = Ppcmd_glue (List.map pr l)
if a strict behavior is needed, use [prlist_strict] instead.
evaluation is done from left to right. *)
-let prlist_sep_lastsep no_empty sep lastsep elem =
- let rec start = function
- |[] -> mt ()
- |[e] -> elem e
- |h::t -> let e = elem h in
- if no_empty && ismt e then start t else
- let rec aux = function
- |[] -> mt ()
- |h::t ->
- let e = elem h and r = aux t in
- if no_empty && ismt e then r else
- if ismt r
- then let s = lastsep () in s ++ e
- else let s = sep () in s ++ e ++ r
- in let r = aux t in e ++ r
- in start
-
+let prlist_sep_lastsep no_empty sep_thunk lastsep_thunk elem l =
+ let sep = sep_thunk () in
+ let lastsep = lastsep_thunk () in
+ let elems = List.map elem l in
+ let filtered_elems =
+ if no_empty then
+ List.filter (fun e -> not (ismt e)) elems
+ else
+ elems
+ in
+ let rec insert_seps es =
+ match es with
+ | [] -> mt ()
+ | [e] -> e
+ | h::[e] -> h ++ lastsep ++ e
+ | h::t -> h ++ sep ++ insert_seps t
+ in
+ insert_seps filtered_elems
+
let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l
(* [prlist_with_sep sep pr [a ; ... ; c]] outputs
[pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
diff --git a/lib/pp.mli b/lib/pp.mli
index be255a74fd..96656c8b65 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -145,7 +145,10 @@ val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val prlist_with_sep :
(unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds
(** [prlist_with_sep sep pr [a ; ... ; c]] outputs
- [pr a ++ sep() ++ ... ++ sep() ++ pr c]. *)
+ [pr a ++ sep () ++ ... ++ sep () ++ pr c].
+ where the thunk sep is memoized, rather than being called each place
+ its result is used.
+*)
val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
(** As [prlist], but on arrays. *)
diff --git a/lib/profile.ml b/lib/profile.ml
index b669161858..0bc226a450 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -85,6 +85,9 @@ let init_alloc = ref 0.0
let reset_profile () = List.iter reset_record !prof_table
let init_profile () =
+ (* We test Flags.profile as a way to support declaring profiled
+ functions in plugins *)
+ if !prof_table <> [] || Flags.profile then begin
let outside = create_record () in
stack := [outside];
last_alloc := get_alloc ();
@@ -92,6 +95,7 @@ let init_profile () =
init_time := get_time ();
outside.tottime <- - !init_time;
outside.owntime <- - !init_time
+ end
let ajoute n o =
o.owntime <- o.owntime + n.owntime;
@@ -317,15 +321,15 @@ let adjust_time ov_bc ov_ad e =
owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
let close_profile print =
- let dw = spent_alloc () in
- let t = get_time () in
- match !stack with
- | [outside] ->
- outside.tottime <- outside.tottime + t;
- outside.owntime <- outside.owntime + t;
- ajoute_ownalloc outside dw;
- ajoute_totalloc outside dw;
- if !prof_table <> [] then begin
+ if !prof_table <> [] then begin
+ let dw = spent_alloc () in
+ let t = get_time () in
+ match !stack with
+ | [outside] ->
+ outside.tottime <- outside.tottime + t;
+ outside.owntime <- outside.owntime + t;
+ ajoute_ownalloc outside dw;
+ ajoute_totalloc outside dw;
let ov_bc = time_overhead_B_C () (* B+C overhead *) in
let ov_ad = time_overhead_A_D () (* A+D overhead *) in
let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
@@ -346,8 +350,8 @@ let close_profile print =
in
if print then format_profile updated_data;
init_profile ()
- end
- | _ -> failwith "Inconsistency"
+ | _ -> failwith "Inconsistency"
+ end
let print_profile () = close_profile true
@@ -358,9 +362,6 @@ let declare_profile name =
prof_table := (name,e)::!prof_table;
e
-(* Default initialization, may be overridden *)
-let _ = init_profile ()
-
(******************************)
(* Entry points for profiling *)
let profile1 e f a =
diff --git a/lib/terminal.ml b/lib/terminal.ml
index 3b6e34f0b8..34efddfbca 100644
--- a/lib/terminal.ml
+++ b/lib/terminal.ml
@@ -35,6 +35,8 @@ type style = {
italic : bool option;
underline : bool option;
negative : bool option;
+ prefix : string option;
+ suffix : string option;
}
let set o1 o2 = match o1 with
@@ -51,9 +53,11 @@ let default = {
italic = None;
underline = None;
negative = None;
+ prefix = None;
+ suffix = None;
}
-let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style () =
+let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style ?prefix ?suffix () =
let st = match style with
| None -> default
| Some st -> st
@@ -65,6 +69,8 @@ let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style () =
italic = set st.italic italic;
underline = set st.underline underline;
negative = set st.negative negative;
+ prefix = set st.prefix prefix;
+ suffix = set st.suffix suffix;
}
let merge s1 s2 =
@@ -75,6 +81,8 @@ let merge s1 s2 =
italic = set s1.italic s2.italic;
underline = set s1.underline s2.underline;
negative = set s1.negative s2.negative;
+ prefix = set s1.prefix s2.prefix;
+ suffix = set s1.suffix s2.suffix;
}
let base_color = function
@@ -168,6 +176,8 @@ let reset_style = {
italic = Some false;
underline = Some false;
negative = Some false;
+ prefix = None;
+ suffix = None;
}
let has_style t =
diff --git a/lib/terminal.mli b/lib/terminal.mli
index dbc418dd6a..b1b76e6e2a 100644
--- a/lib/terminal.mli
+++ b/lib/terminal.mli
@@ -35,11 +35,14 @@ type style = {
italic : bool option;
underline : bool option;
negative : bool option;
+ prefix : string option;
+ suffix : string option;
}
val make : ?fg_color:color -> ?bg_color:color ->
?bold:bool -> ?italic:bool -> ?underline:bool ->
- ?negative:bool -> ?style:style -> unit -> style
+ ?negative:bool -> ?style:style ->
+ ?prefix:string -> ?suffix:string -> unit -> style
(** Create a style from the given flags. It is derived from the optional
[style] argument if given. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:45:16 +0000