diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 2 | ||||
| -rw-r--r-- | lib/pp.ml | 13 |
2 files changed, 6 insertions, 9 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 @@ -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] *) |