readded function box_of

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 30847816982ceb501d202ffb5152b846b7cb5a6e..6bcec8edd4d722062d71f986a19a3edd7e069354 100644 (file)
--- 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