From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Jul 2008 19:05:12 +0000 (+0000)
Subject: Rendering of \infrule improved.
X-Git-Tag: make_still_working~4902
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=29dce796091e98b5bfe48423189453eaad449bda;p=helm.git

Rendering of \infrule improved.
---

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 8ed430901..abd7ab041 100644
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -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)