From c0e81c0055dc03a8798c45b6c41673bc3ee69d5d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 07:55:05 +0000 Subject: [PATCH] better boxes (with more line breaking hints) for objects rendering --- .../ocaml/cic_transformations/content2pres.ml | 24 ++++++++++++------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index e73e4ec33..ee3e64bd5 100644 --- 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 = -- 2.39.2