From cb0c0fe95610321224311a64aef214775d36e7e4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 May 2011 10:34:09 +0000 Subject: [PATCH] want_indent bug fixed --- matitaB/components/content_pres/boxPp.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml index 9bf360a63..9511de631 100644 --- a/matitaB/components/content_pres/boxPp.ml +++ b/matitaB/components/content_pres/boxPp.ml @@ -32,7 +32,7 @@ let utf8_string_length s = Utf8.compute_len s 0 (String.length s) let string_space = " " let string_space_len = utf8_string_length string_space -let string_indent = (* string_space *) "" +let string_indent = (* string_space *) " " let string_indent_len = utf8_string_length string_indent let string_ink = "---------------------------" let string_ink_len = utf8_string_length string_ink @@ -40,8 +40,10 @@ let string_ink_len = utf8_string_length string_ink let contains_attrs contained container = List.for_all (fun attr -> List.mem attr container) contained -let want_indent = contains_attrs (* (RenderingAttrs.indent_attributes `BoxML) *)[] -let want_spacing = contains_attrs (* (RenderingAttrs.spacing_attributes `BoxML) *) [] +let small_skip_attributes _ = [ None, "width", "0.5em" ] + +let want_indent = contains_attrs [ None, "indent", "0.5em" ] +let want_spacing = contains_attrs [ None, "spacing", "0.5em" ] let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);; -- 2.39.2