From: Kim Nguyễn <kn@lri.fr>
Date: Mon, 4 Mar 2013 17:53:38 +0000 (+0100)
Subject: Simply use String.make for Pretty.padding and Pretty.line, since it's
X-Git-Tag: v0.1~171
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=d16314f40989a63bbd1119a9701fa44e336599ff

Simply use String.make for Pretty.padding and Pretty.line, since it's
only used in places where performance is not critical.
---

diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml
index c54d0ed..abcb59c 100644
--- a/src/utils/pretty.ml
+++ b/src/utils/pretty.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-01-30 19:08:11 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-04 18:46:09 CET by Kim Nguyen>
 *)
 
 open Format
@@ -112,12 +112,12 @@ let strike s = combine_all combining_stroke s
 
 let mk_repeater c =
   let mk_str i = String.make i c in
-  let _table = Array.init 16 mk_str in
+  let _table = Array.init 256 mk_str in
      fun i -> try
       if i < 16 then _table.(i) else mk_str i
     with e -> print_int i; print_newline(); raise e
-let padding = mk_repeater ' '
-let line = mk_repeater '_'
+let padding i = String.make i ' '
+let line i = String.make i '_'