notation with mstyle attributes, like colors and size

[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 abd7ab0410b628de77835376ea2186c2136a73e1..e6cbbf692be37411ab8c1ee8c1f10e465179cae6 100644 (file)
--- 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 
@@ -399,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