let c1 = current_size + (String.length name) in
countsubst subst c1
| CE.LocalVar (_,name) -> current_size + (String.length name)
- | CE.Meta (_,name) -> current_size + (String.length name)
+ | CE.Meta (_,name,l) ->
+ List.fold_left
+ (fun i t ->
+ match t with
+ None -> i
+ | Some t' -> aux i t'
+ ) (current_size + String.length name) l
| CE.Num (_,value) -> current_size + (String.length value)
| CE.Appl (_,l) ->
List.fold_left aux current_size l
if tail = [] then
P.Mi (attr,name)
else P.Mrow([],P.Mi (attr,name)::tail)
- | CE.Meta (xref,name) ->
+ | CE.Meta (xref,name,l) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::tail)
+ let l' =
+ List.map
+ (function
+ None -> P.Mo([],"_")
+ | Some t -> cexpr2pres t
+ ) l
+ in
+ if tail = [] then
+ P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+ else
+ P.Mrow
+ ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
| CE.Num (xref,value) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
if tail = [] then
P.Mi (attr,name)
else P.Mrow ([],P.Mi (attr,name)::tail)
- | CE.Meta (xref,name) ->
+ | CE.Meta (xref,name,l) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow ([],P.Mi (attr,name)::tail)
+ let l' =
+ List.map
+ (function
+ None -> P.Mo([],"_")
+ | Some t -> cexpr2pres t
+ ) l
+ in
+ if tail = [] then
+ P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+ else
+ P.Mrow
+ ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
| CE.Num (xref,value) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then