- | A.AttributedTerm (`Loc _, t) -> return (invoke mathonly xref prec assoc t)
- | A.AttributedTerm (`Level (prec, assoc), t) ->
- return (invoke mathonly xref prec assoc t)
- | A.AttributedTerm (`IdRef xref, t) ->
- return (invoke mathonly (Some xref) prec assoc t)
-
- | A.Ident (literal, _) -> return (P.Mi (make_href xref, to_unicode literal))
- | A.Num (literal, _) -> return (P.Mn (make_href xref, to_unicode literal))
- | A.Symbol (literal, _) -> return (P.Mo (make_href xref,to_unicode literal))
- | A.Uri (literal, _) -> return (P.Mi (make_href xref, to_unicode literal))
-
- (* default pretty printing shant' be implemented here *)
-(* | A.Appl terms ->
- let children = aux_children mathonly xref prec assoc terms in
- make_hv xref children
- | A.Binder (`Pi, (A.Ident ("_", None), ty_opt), body)
- | A.Binder (`Forall, (A.Ident ("_", None), ty_opt), body) ->
- let ty' =
- match ty_opt with
- | None -> mpres_implicit
- | Some ty -> invoke mathonly None prec assoc ty
- in
- let body' = invoke mathonly None prec assoc body in
- return (make_hv xref [ty'; make_h None [mpres_arrow; body']]) *)
-
- | A.Literal l -> aux_literal xref prec assoc l
- | A.Layout l -> aux_layout mathonly xref prec assoc l
+ | A.AttributedTerm (attr, t) ->
+ aux_attribute xmlattrs mathonly xref pos prec uris t attr
+ | A.Ident (literal, _) ->
+ P.Mi (make_href xmlattrs xref [], to_unicode literal)
+ | A.Num (literal, _) ->
+ P.Mn (make_href xmlattrs xref [], to_unicode literal)
+ | A.Symbol (literal, _) ->
+ P.Mo (make_href xmlattrs xref uris, to_unicode literal)
+ | A.Uri (literal, _) ->
+ P.Mi (make_href xmlattrs xref [], to_unicode literal)
+ | A.Literal l -> aux_literal xmlattrs xref prec uris l
+ | A.Layout l -> aux_layout mathonly xref pos prec uris l