Simply use String.make for Pretty.padding and Pretty.line, since it's

[tatoo.git] / src / utils / pretty.ml

diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml
index c54d0ed..abcb59c 100644 (file)
--- 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 '_'