diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | lib/pp.ml | 13 | ||||
| -rw-r--r-- | lib/stateid.ml | 2 | ||||
| -rw-r--r-- | lib/stateid.mli | 1 | ||||
| -rw-r--r-- | lib/system.ml | 6 | ||||
| -rw-r--r-- | lib/system.mli | 2 |
8 files changed, 19 insertions, 15 deletions
diff --git a/lib/control.ml b/lib/control.ml index e09068740d..ffb3584f1e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -57,7 +57,7 @@ let windows_timeout n f x e = done in let init = Unix.gettimeofday () in - let _id = Thread.create thread init in + let _id = CThread.create thread init in try let res = f x in let () = killed := true in diff --git a/lib/flags.ml b/lib/flags.ml index ae4d337ded..55bfa3cbde 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -66,7 +66,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 = V8_7 | V8_8 | Current +type compat_version = V8_7 | V8_8 | V8_9 | Current let compat_version = ref Current @@ -77,6 +77,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_8, V8_8 -> 0 | V8_8, _ -> -1 | _, V8_8 -> 1 + | V8_9, V8_9 -> 0 + | V8_9, _ -> -1 + | _, V8_9 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -85,6 +88,7 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_7 -> "8.7" | V8_8 -> "8.8" + | V8_9 -> "8.9" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index d883cf1e30..7336b9beaf 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -58,7 +58,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_7 | V8_8 | Current +type compat_version = V8_7 | V8_8 | V8_9 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool @@ -284,15 +284,12 @@ let pr_vertical_list pr = function [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) let prvecti_with_sep sep elem v = - let rec pr i = - if Int.equal i 0 then - elem 0 v.(0) - else - let r = pr (i-1) and s = sep () and e = elem i v.(i) in - r ++ s ++ e + let v = CArray.mapi (fun i x -> + let pp = if i = 0 then mt() else sep() in + pp ++ elem i x) + v in - let n = Array.length v in - if Int.equal n 0 then mt () else pr (n - 1) + seq (Array.to_list v) (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) diff --git a/lib/stateid.ml b/lib/stateid.ml index 5485c4bf19..8f45f3605d 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -27,6 +27,8 @@ let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare +let print id = Pp.int id + module Self = struct type t = int let compare = compare diff --git a/lib/stateid.mli b/lib/stateid.mli index 5d4b71a354..f6ce7ddc40 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -20,6 +20,7 @@ val initial : t val dummy : t val fresh : unit -> t val to_string : t -> string +val print : t -> Pp.t val of_int : int -> t val to_int : t -> int diff --git a/lib/system.ml b/lib/system.ml index a9db95318f..fd6579dd69 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -287,20 +287,20 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (round (sstop -. sstart)) ++ str "s" ++ str ")" -let with_time ~batch f x = +let with_time ~batch ~header f x = let tstart = get_time() in let msg = if batch then "" else "Finished transaction in " in try let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) diff --git a/lib/system.mli b/lib/system.mli index a3b79ee528..6dd1eb5a84 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -105,7 +105,7 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t -val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b +val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b (** [get_toplevel_path program] builds a complete path to the executable denoted by [program]. This involves: |