X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaEngine.ml;h=144250fb9b55e634312523693f15f1c309d8add5;hb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;hp=5d16763fc36ad6db0b685937e47e53fdc11e2c5b;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 5d16763fc..144250fb9 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -71,15 +71,17 @@ let cut prefix s = String.sub s lenp (lens-lenp) ;; -let print_string = +let print_string = let indent = ref 0 in let print_string ~right_justify s = let ss = match right_justify with None -> "" | Some (ss,len_ss) -> - String.make (80 - !indent - len_ss - String.length s) ' ' ^ ss + let i = 80 - !indent - len_ss - String.length s in + if i > 0 then String.make i ' ' ^ ss else ss in + assert (!indent >=0); print_string (String.make !indent ' ' ^ s ^ ss) in fun enter ?right_justify s -> if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)