X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=e6cbbf692be37411ab8c1ee8c1f10e465179cae6;hb=e7759b1c1f40380748ac052bce5b677bc8fd71cb;hp=8ed430901893a0d2cf8f268b34c6509428e30fbd;hpb=d063ddede0424eb1f47a4c9769eaefbb16d90700;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 8ed430901..e6cbbf692 100644
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -344,7 +344,7 @@ let render ids_to_uris ?(prec=(-1)) =
             | Some prec -> prec
           in
           (match !inferred_level with
-          | None -> aux !new_xmlattrs mathonly new_xref prec t 
+          | None -> aux !new_xmlattrs mathonly new_xref prec t
           | Some child_prec ->
               let t' = aux !new_xmlattrs mathonly new_xref child_prec t in
               (*prerr_endline 
@@ -381,11 +381,15 @@ let render ids_to_uris ?(prec=(-1)) =
         Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1,
           invoke_reinit t2)
     | A.InfRule (t1, t2, t3) ->
+      Mpres.Mstyle ([None,"mathsize","big"],
        Mpres.Mrow (attrs,
         [Mpres.Mfrac ([],
            Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1),
            Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2));
-         Mpres.Mstyle ([None,"scriptlevel","2"],invoke_reinit t3)])
+          Mpres.Mstyle ([None,"scriptlevel","2"],
+           Mpresentation.Mspace 
+            (RenderingAttrs.small_skip_attributes `MathML));
+         Mpres.Mstyle ([None,"scriptlevel","1"],invoke_reinit t3)]))
     | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t)
     | A.Root (t1, t2) ->
         Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2)
@@ -395,6 +399,12 @@ let render ids_to_uris ?(prec=(-1)) =
             (CicNotationUtil.ungroup terms)
         in
         box_of mathonly kind attrs children
+    | A.Mstyle (l,terms) -> 
+        Mpres.Mstyle 
+          (List.map (fun (k,v) -> None,k,v) l, 
+           box_of mathonly (A.H, false, false) attrs 
+            (aux_children mathonly false xref  prec 
+              (CicNotationUtil.ungroup terms)))
     | A.Group terms ->
 	let children =
           aux_children mathonly false xref  prec