X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommOutput.ml;h=e0f3f1d70397327d87a3dd60e1181a238e44cdb7;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=5189c7f7790141b113491e39e3c4d2085e299d86;hpb=baa54e5db0fb93c4242dd1b67a5018ca63206cf6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml index 5189c7f77..e0f3f1d70 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml @@ -2,8 +2,19 @@ module ET = RecommTypes let width = ref 78 +let replace = ref false + +let string_length_utf8 s = + let l = String.length s in + let rec aux r i = + if i >= l then r else + if '\x80' <= s.[i] && s.[i] <= '\xBF' + then aux (succ r) (succ i) else aux r (succ i) + in + l - aux 0 0 + let complete s = - let l = !width - String.length s - 6 in + let l = !width - string_length_utf8 s - 6 in if l < 0 then begin Printf.eprintf "overfull: %S\n" s; "" @@ -17,9 +28,9 @@ let out_src och = function | ET.Text s -> Printf.fprintf och "%s" s | ET.Mark s -> - Printf.fprintf och "(* %s**)" s + Printf.fprintf och "(* *%s*)" s | ET.Key (s1, s2) -> - Printf.fprintf och "(* %s1%s2*)" s1 s2 + Printf.fprintf och "(* %s%s*)" s1 s2 | ET.Title ss -> let s = String.concat " " ss in Printf.fprintf och "(* %s %s*)" s (complete s) @@ -30,6 +41,14 @@ let out_src och = function Printf.fprintf och "%s%s%s" s1 s2 s3 let write_srcs file srcs = - let och = open_out (file ^ ".new") in + let target = + if !replace then begin + Sys.rename file (file ^ ".old"); + file + end else begin + file ^ ".new" + end + in + let och = open_out target in List.iter (out_src och) srcs; close_out och