+ let attrs =
+ (RenderingAttrs.symbol_attributes `MathML)
+ @ make_href xmlattrs xref uris
+ in
+ P.Mo (attrs, to_unicode literal)
+ | A.Ident (literal, subst)
+ | A.Uri (literal, subst) ->
+ let attrs =
+ (RenderingAttrs.ident_attributes `MathML)
+ @ make_href xmlattrs xref []
+ in
+ let name = P.Mi (attrs, to_unicode literal) in
+ (match subst with
+ | Some []
+ | None -> name
+ | Some substs ->
+ let substs' =
+ box_of mathonly (A.H, false, false) []
+ (open_brace
+ :: (CicNotationUtil.dress semicolon
+ (List.map
+ (fun (name, t) ->
+ box_of mathonly (A.H, false, false) [] [
+ P.Mi ([], name);
+ P.Mo ([], to_unicode "\\def");
+ aux [] mathonly xref pos prec uris t ])
+ substs))
+ @ [ closed_brace ])
+(* (CicNotationUtil.dress semicolon
+ (List.map
+ (fun (var, t) ->
+ let var_uri = UriManager.uri_of_string var in
+ let var_name = UriManager.name_of_uri var_uri in
+ let href_attr = Some "xlink", "href", var in
+ box_of mathonly (A.H, false, false) [] [
+ P.Mi ([href_attr], var_name);
+ P.Mo ([], to_unicode "\\def");
+ aux [] mathonly xref pos prec uris t ])
+ substs)) *)
+ in
+ let substs_maction = toggle_action [ hidden_substs; substs' ] in
+ box_of mathonly (A.H, false, false) [] [ name; substs_maction ])