]> matita.cs.unibo.it Git - helm.git/commitdiff
better boxes (with more line breaking hints) for objects rendering
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 27 Jul 2005 07:55:05 +0000 (07:55 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 27 Jul 2005 07:55:05 +0000 (07:55 +0000)
helm/ocaml/cic_transformations/content2pres.ml

index e73e4ec33186a0c420259e31cfc56a3e96cfa1f0..ee3e64bd5456d873e0af5f74ca00f2c6213ab5b9 100644 (file)
@@ -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 =