X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPres.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationPres.ml;h=7c87dedce0168ecc76d7d954d782d592fe48b6e4;hb=206f96afb7097c20b3cc8bd144825467b4fde7ae;hp=e7afad578387bd64d156b89991e3b4ed7c2d99e5;hpb=e80eed78f048a235b44d2fd266c4b5a4dd951632;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index e7afad578..7c87dedce 100644
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+module P = Mpresentation
+
 type mathml_markup = boxml_markup Mpresentation.mpres
 and boxml_markup = mathml_markup Box.box
 
@@ -69,7 +71,8 @@ let rec promote_to_math =
   | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> promote_to_math mpres
   | math -> math
 
-let small_skip = Mpresentation.Mspace [None, "width", "0.5em"]
+let small_skip =
+  Mpresentation.Mspace (RenderingAttrs.small_skip_attributes `MathML)
 
 let box_of mathonly spec attrs children =
   match children with
@@ -85,8 +88,8 @@ let box_of mathonly spec attrs children =
 	  if mathonly then Mpresentation.Mrow (attrs, dress children)
 	  else
             let attrs' =
-	      (if spacing then [None, "spacing", "0.5em"] else [])
-              @ (if indent then [None, "indent", "0.5em"] else [])
+	      (if spacing then RenderingAttrs.spacing_attributes `BoxML else [])
+              @ (if indent then RenderingAttrs.indent_attributes `BoxML else [])
               @ attrs
             in
               match kind with
@@ -136,7 +139,6 @@ let pp_pos =
     | `Inner -> "`Inner"
 
 let is_atomic t =
-  let module P = Mpresentation in
   let rec aux_mpres = function
     | P.Mi _
     | P.Mo _
@@ -204,8 +206,8 @@ let render ids_to_uris =
   (* when mathonly is true no boxes should be generated, only mrows *)
   let rec aux xmlattrs mathonly xref pos prec uris t =
     match t with
-    | A.AttributedTerm (attr, t) ->
-        aux_attribute xmlattrs mathonly xref pos prec uris t attr
+    | A.AttributedTerm _ ->
+        aux_attributes xmlattrs mathonly xref pos prec uris t
     | A.Num (literal, _) ->
         let attrs =
           (RenderingAttrs.number_attributes `MathML)
@@ -263,8 +265,34 @@ let render ids_to_uris =
     | t ->
         prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t);
         assert false
-  and aux_attribute xmlattrs mathonly xref pos prec uris t =
-    function
+  and aux_attributes xmlattrs mathonly xref pos prec uris t =
+    let new_level = ref None in
+    let new_xref = ref None in
+    let new_uris = ref [] in
+    let new_xmlattrs = ref [] in
+    let rec aux_attribute =
+      function
+      | A.AttributedTerm (attr, t) ->
+          (match attr with
+          | `Loc _
+          | `Raw _ -> ()
+          | `Level (child_prec, child_assoc) ->
+              new_level := Some (child_prec, child_assoc)
+          | `IdRef xref -> new_xref := Some xref
+          | `Href hrefs -> new_uris := hrefs
+          | `XmlAttrs attrs -> new_xmlattrs := attrs);
+          aux_attribute t
+      | t ->
+          (match !new_level with
+          | None -> aux !new_xmlattrs mathonly !new_xref pos prec !new_uris t
+          | Some (child_prec, child_assoc) ->
+              let t' = 
+                aux !new_xmlattrs mathonly !new_xref pos child_prec !new_uris t
+              in
+              add_parens child_prec child_assoc pos prec t')
+    in
+    aux_attribute t
+(*     function
     | `Loc _
     | `Raw _ -> aux xmlattrs mathonly xref pos prec uris t
     | `Level (child_prec, child_assoc) ->
@@ -272,7 +300,7 @@ let render ids_to_uris =
         add_parens child_prec child_assoc pos prec t'
     | `IdRef xref -> aux xmlattrs mathonly (Some xref) pos prec uris t
     | `Href uris' -> aux xmlattrs mathonly xref pos prec uris' t
-    | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t
+    | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t *)
   and aux_literal xmlattrs xref prec uris l =
     let attrs = make_href xmlattrs xref uris in
     (match l with
@@ -358,7 +386,9 @@ let rec print_box (t: CicNotationPres.boxml_markup) =
 and print_mpres (t: CicNotationPres.mathml_markup) =
   Mpresentation.print_mpres print_box t
 
-let render_to_boxml id_to_uri t =
+let print_xml = print_mpres
+
+(* let render_to_boxml id_to_uri t =
   let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
-  Xml.add_xml_declaration xml_stream
+  Xml.add_xml_declaration xml_stream *)