diff options
author | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-29 22:13:42 +0000 |
---|---|---|
committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-29 22:13:42 +0000 |
commit | 7492cf1e20f39dab6f721b10332c1f4fcfb7c42f (patch) | |
tree | 11d83e6e8f93e0f8bb1733c02bb03ed3120f43a9 /checklink/Library.ml | |
parent | 152660e35ef5bf1bfba11b20bc8654a6394531fc (diff) | |
download | compcert-7492cf1e20f39dab6f721b10332c1f4fcfb7c42f.tar.gz compcert-7492cf1e20f39dab6f721b10332c1f4fcfb7c42f.zip |
checklink: Faster printing
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Library.ml')
-rw-r--r-- | checklink/Library.ml | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml index f6b18835..b6f48aef 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -113,18 +113,17 @@ let z_int_lax z = Safe32.to_int (z_int32_lax z) (* Some more printers *) let string_of_array string_of_elt sep a = - let contents = - (fst - (Array.fold_left - (fun accu elt -> - let (str, ndx) = accu in - (str ^ (if ndx > 0 then sep else "") ^ string_of_int ndx ^ ": " ^ - string_of_elt elt, ndx + 1) - ) - ("", 0) a - ) - ) - in "[\n" ^ contents ^ "\n]" + let b = Buffer.create 1024 in + Buffer.add_string b "[\n"; + Array.iteri + (fun ndx elt -> + if ndx > 0 then Buffer.add_string b sep; + Buffer.add_string b (string_of_int ndx); + Buffer.add_string b ": "; + Buffer.add_string b (string_of_elt elt) + ) a; + Buffer.add_string b "\n]"; + Buffer.contents b let string_of_list string_of_elt sep l = String.concat sep (List.map string_of_elt l) |