better boxes (with more line breaking hints) for objects rendering

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index e73e4ec33186a0c420259e31cfc56a3e96cfa1f0..ee3e64bd5456d873e0af5f74ca00f2c6213ab5b9 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -58,19 +58,25 @@ let get_xref = function
   | `Definition d -> d.Con.def_id
   | `Joint jo -> jo.Con.joint_id
 
-let make_row ?(attrs=[]) items concl =
-  match concl with 
-      B.V _ -> (* big! *)
+let hv_attrs =
+  RenderingAttrs.spacing_attributes `BoxML
+  @ RenderingAttrs.indent_attributes `BoxML
+
+let make_row items concl =
+  B.b_hv hv_attrs (items @ [ concl ])
+(*   match concl with 
+      B.V _ -> |+ big! +|
         B.b_v attrs [B.b_h [] items; B.b_indent concl]
-    | _ ->  (* small *)
-       B.b_h attrs (items@[B.b_space; concl])
+    | _ ->  |+ small +|
+        B.b_h attrs (items@[B.b_space; concl]) *)
 
 let make_concl ?(attrs=[]) verb concl =
-  match concl with 
-      B.V _ -> (* big! *)
+  B.b_hv (hv_attrs @ attrs) [ B.b_kw verb; concl ]
+(*   match concl with 
+      B.V _ -> |+ big! +|
         B.b_v attrs [ B.b_kw verb; B.b_indent concl]
-    | _ ->  (* small *)
-       B.b_h attrs [ B.b_kw verb; B.b_space; concl ]
+    | _ ->  |+ small +|
+        B.b_h attrs [ B.b_kw verb; B.b_space; concl ] *)
 
 let make_args_for_apply term2pres args =
  let make_arg_for_apply is_first arg row =