From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 May 2011 10:34:09 +0000 (+0000)
Subject: want_indent bug fixed
X-Git-Tag: make_still_working~2500
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb0c0fe95610321224311a64aef214775d36e7e4;p=helm.git

want_indent bug fixed
---

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);;