- and aux_attribute xmlattrs mathonly xref pos prec uris t =
- function
- | `Loc _ -> aux xmlattrs mathonly xref pos prec uris t
- | `Level (child_prec, child_assoc) ->
- let t' = aux xmlattrs mathonly xref pos child_prec uris t in
- add_parens child_prec child_assoc pos prec t'
- | `IdRef xref -> aux xmlattrs mathonly (Some xref) pos prec uris t
- | `Href uris' -> aux xmlattrs mathonly xref pos prec uris' t
- | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t
- and aux_literal xmlattrs xref prec uris l =
- let attrs = make_href xmlattrs xref uris in
- match l with
- | `Symbol s -> P.Mo (attrs, to_unicode s)
- | `Keyword s -> P.Mo (attrs, to_unicode s)
- | `Number s -> P.Mn (attrs, to_unicode s)
- and aux_layout mathonly xref pos prec uris l =
+ and aux_attributes xmlattrs mathonly xref pos prec t =
+ let reset = ref false in
+ let new_level = ref None in
+ let new_xref = ref [] in
+ let new_xmlattrs = ref [] in
+ let new_pos = ref pos in
+ let reinit = ref false in
+ let rec aux_attribute =
+ function
+ | A.AttributedTerm (attr, t) ->
+ (match attr with
+ | `Loc _
+ | `Raw _ -> ()
+ | `Level (-1, _) -> reset := true
+ | `Level (child_prec, child_assoc) ->
+ new_level := Some (child_prec, child_assoc)
+ | `IdRef xref -> new_xref := xref :: !new_xref
+ | `ChildPos pos -> new_pos := pos
+ | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
+ aux_attribute t
+ | t ->
+ (match !new_level with
+ | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
+ | Some (child_prec, child_assoc) ->
+ let t' =
+ aux !new_xmlattrs mathonly new_xref !new_pos child_prec t
+ in
+ if !reset then t'
+ else add_parens child_prec child_assoc !new_pos prec t')
+ in
+ aux_attribute t
+ and aux_literal xmlattrs xref prec l =
+ let attrs = make_href xmlattrs xref in
+ (match l with
+ | `Symbol s -> Mpres.Mo (attrs, to_unicode s)
+ | `Keyword s -> Mpres.Mo (attrs, to_unicode s)
+ | `Number s -> Mpres.Mn (attrs, to_unicode s))
+ and aux_layout mathonly xref pos prec l =