From 7492cf1e20f39dab6f721b10332c1f4fcfb7c42f Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 29 Jun 2012 22:13:42 +0000
Subject: checklink: Faster printing

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Library.ml | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

(limited to 'checklink/Library.ml')

diff --git a/checklink/Library.ml b/checklink/Library.ml
index f6b1883..b6f48ae 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)
-- 
cgit v1.2.3