]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationPres.ml
maction layout added to notation
[helm.git] / helm / software / components / content_pres / cicNotationPres.ml
index 77dc2b08cf8c52ebfcf2fb7f49b8e98f2eaa6903..1a092909e113cdafcd00343281d5b9192c2056b8 100644 (file)
@@ -405,6 +405,14 @@ let render ids_to_uris ?(prec=(-1)) =
            box_of mathonly (A.H, false, false) attrs 
             (aux_children mathonly false xref  prec 
               (CicNotationUtil.ungroup terms)))
+    | A.Mpadded (l,terms) -> 
+        Mpres.Mpadded 
+          (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.Maction alternatives -> 
+         toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms ->
        let children =
           aux_children mathonly false xref  prec