From 33cef65313289250ea37c782c65306f7c967cd04 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 May 2011 10:06:00 +0000 Subject: [PATCH] readded function box_of --- .../content_pres/cicNotationPres.ml | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index 308478169..6bcec8edd 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -31,6 +31,7 @@ type markup = string Box.box let to_unicode = Utf8Macro.unicode_of_tex +let small_skip = Box.Text ([], " ") let open_paren = Box.Text ([], "(") let closed_paren = Box.Text ([], ")") let semicolon = Box.Text ([], ";") @@ -74,6 +75,28 @@ let add_parens child_prec curr_prec t = BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) +let box_of spec attrs children = + match children with + | [t] -> t + | _ -> + let kind, spacing, indent = spec in + let dress children = + if spacing then + NotationUtil.dress small_skip children + else + children + in + let attrs' = + (if spacing then RenderingAttrs.spacing_attributes `BoxML else []) + @ (if indent then RenderingAttrs.indent_attributes `BoxML else []) + @ attrs + in + match kind with + | A.H -> Box.H (attrs',children) + | A.V -> Box.V (attrs',children) + | A.HV -> Box.HV (attrs',children) + | A.HOV -> Box.HOV (attrs',children) + let render status ?(prec=(-1)) = let rec aux prec t = match t with -- 2.39.2