added {get,set}_attr

diff --git a/helm/ocaml/cic_notation/mpresentation.ml b/helm/ocaml/cic_notation/mpresentation.ml
index 69d4fd9a0de334585e6cabce76552b00af1aea7d..db05f31bea0dfc9cd121bda41c3814bbe8befb6e 100644 (file)
--- a/helm/ocaml/cic_notation/mpresentation.ml
+++ b/helm/ocaml/cic_notation/mpresentation.ml
@@ -190,3 +190,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)
+

diff --git a/helm/ocaml/cic_notation/mpresentation.mli b/helm/ocaml/cic_notation/mpresentation.mli
index e322e92e12de2c8dc433328372aea69c0cddb777..8252517a67ae1eb04912f116f8ad4260423540dc 100644 (file)
--- a/helm/ocaml/cic_notation/mpresentation.mli
+++ b/helm/ocaml/cic_notation/mpresentation.mli
@@ -66,6 +66,9 @@ and attr = (string option * string * string) list
 
 ;;
 
+val get_attr: 'a mpres -> attr
+val set_attr: attr -> 'a mpres -> 'a mpres
+
 val smallskip : 'a mpres 
 val indented : 'a mpres -> 'a mpres
 val standard_tbl_attr : attr