]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/mpresentation.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_notation / mpresentation.ml
index 69d4fd9a0de334585e6cabce76552b00af1aea7d..1303d1eb7a4dc19d4effa0122074b13c54d002d1 100644 (file)
@@ -108,7 +108,14 @@ let print_mpres obj_printer mpres =
     function
       Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s)
     | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s)
-    | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
+    | Mo (attr,s) ->
+        let s =
+          let len = String.length s in
+          if len > 1 && s.[0] = '\\'
+          then String.sub s 1 (len - 1)
+          else s
+        in
+        X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
     | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s)
     | Mspace attr -> X.xml_empty ~prefix "mspace" attr
     | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s)
@@ -190,3 +197,60 @@ let document_of_mpres pres =
      "rowspacing", "0.6ex"] (print_mpres (fun _ -> assert false) pres))
  >]
 
+let get_attr = function
+  | Maction (attr, _)
+  | Menclose (attr, _)
+  | Merror (attr, _)
+  | Mfenced (attr, _)
+  | Mfrac (attr, _, _)
+  | Mgliph (attr, _)
+  | Mi (attr, _)
+  | Mn (attr, _)
+  | Mo (attr, _)
+  | Mobject (attr, _)
+  | Mover (attr, _, _)
+  | Mpadded (attr, _)
+  | Mphantom (attr, _)
+  | Mroot (attr, _, _)
+  | Mrow (attr, _)
+  | Ms (attr, _)
+  | Mspace attr
+  | Msqrt (attr, _)
+  | Mstyle (attr, _)
+  | Msub (attr, _, _)
+  | Msubsup (attr, _, _, _)
+  | Msup (attr, _, _)
+  | Mtable (attr, _)
+  | Mtext (attr, _)
+  | Munder (attr, _, _)
+  | Munderover (attr, _, _, _) ->
+      attr
+
+let set_attr attr = function
+  | Maction (_, x) -> Maction (attr, x)
+  | Menclose (_, x) -> Menclose (attr, x)
+  | Merror (_, x) -> Merror (attr, x)
+  | Mfenced (_, x) -> Mfenced (attr, x)
+  | Mfrac (_, x, y) -> Mfrac (attr, x, y)
+  | Mgliph (_, x) -> Mgliph (attr, x)
+  | Mi (_, x) -> Mi (attr, x)
+  | Mn (_, x) -> Mn (attr, x)
+  | Mo (_, x) -> Mo (attr, x)
+  | Mobject (_, x) -> Mobject (attr, x)
+  | Mover (_, x, y) -> Mover (attr, x, y)
+  | Mpadded (_, x) -> Mpadded (attr, x)
+  | Mphantom (_, x) -> Mphantom (attr, x)
+  | Mroot (_, x, y) -> Mroot (attr, x, y)
+  | Mrow (_, x) -> Mrow (attr, x)
+  | Ms (_, x) -> Ms (attr, x)
+  | Mspace _ -> Mspace attr
+  | Msqrt (_, x) -> Msqrt (attr, x)
+  | Mstyle (_, x) -> Mstyle (attr, x)
+  | Msub (_, x, y) -> Msub (attr, x, y)
+  | Msubsup (_, x, y, z) -> Msubsup (attr, x, y, z)
+  | Msup (_, x, y) -> Msup (attr, x, y)
+  | Mtable (_, x) -> Mtable (attr, x)
+  | Mtext (_, x) -> Mtext (attr, x)
+  | Munder (_, x, y) -> Munder (attr, x, y)
+  | Munderover (_, x, y, z) -> Munderover (attr, x, y, z)
+