...

[helm.git] / helm / software / components / content_pres / cicNotationPres.ml

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 728651acc6f2be52523302352c46b0eaf81ec34f..abd7ab0410b628de77835376ea2186c2136a73e1 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -380,6 +380,16 @@ let render ids_to_uris ?(prec=(-1)) =
     | A.Atop (t1, t2) ->
         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"],
+           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)