From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 2 Oct 2009 09:45:52 +0000 (+0000)
Subject: better nlet rec boxing
X-Git-Tag: make_still_working~3398
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38ec119c163b0e6f97a9800933d5b71c065332e8;p=helm.git

better nlet rec boxing
---

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index c88f87535..05e4ae3cb 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -958,11 +958,14 @@ let definition2pres ?recno term2pres d =
       params
   in
   B.b_hv [] 
-   [B.b_hv [] 
-    ([ B.b_space; B.b_text [] name; B.b_space ] @ params @
-    (if rno <> -1 then [B.b_kw "on" ; B.b_space; term2pres rec_param ] else [])
-    @[ B.b_space;
-       B.b_text [] ":"; B.b_space; term2pres ty]); 
+   [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
+    ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @ 
+        [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])] 
+      @ [B.b_h [] 
+         ((if rno <> -1 then 
+           [B.b_kw "on";B.b_space;term2pres rec_param] else [])
+         @ [ B.b_space; B.b_text [] ":";]) ]
+      @[ B.indent(term2pres ty)]); 
    B.b_text [] ":=";
    B.b_h [] [B.b_space;term2pres body] ]
 ;;