]> matita.cs.unibo.it Git - helm.git/commitdiff
better nlet rec boxing
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 2 Oct 2009 09:45:52 +0000 (09:45 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 2 Oct 2009 09:45:52 +0000 (09:45 +0000)
helm/software/components/content_pres/content2pres.ml

index c88f87535f71fe71aa6aac2e539060ad8cea7ae6..05e4ae3cbd8d55532a9cb51ba41b3324989f8389 100644 (file)
@@ -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] ]
 ;;