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
function
[] -> []
| None::tl -> make_attributes (List.tl l1) tl
- | (Some s)::tl -> (List.hd l1,s)::(make_attributes (List.tl l1) tl)
+ | (Some s)::tl ->
+ let p,n = List.hd l1 in
+ (p,n,s)::(make_attributes (List.tl l1) tl)
;;
let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
CE.Symbol (xref,name,None,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow([],P.Mi (attr,name)::tail)
| CE.Symbol (xref,name,Some subst,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
let rec make_subst =
(function
[] -> assert false
(make_subst subst)@
(P.Mtext([],"]")::tail))
| CE.LocalVar (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::tail)
- | CE.Meta (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow([],P.Mi (attr,name)::tail)
+ | CE.Meta (xref,name,l) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ 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 ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mn (attr,value)
else P.Mrow([],P.Mn (attr,value)::tail)
| CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes ["helm:xref"] [axref] in
- let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
+ let aattr = make_attributes [Some "helm","xref"] [axref] in
+ let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
(try
(let f = Hashtbl.find symbol_table n in
f tl ~priority ~assoc ~tail aattr sattr)
P.Mrow(aattr,
P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
| CE.Appl (xref,l) as t ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some"helm","xref"] [xref] in
P.Mrow(attr,
P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
| CE.Binder (xref, kind,(n,s),body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let binder =
if kind = "Lambda" then
Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
Netconversion.ustring_of_uchar `Enc_utf8 0x2203
else "unknown" in
P.Mrow (attr,
- P.Mtext([("mathcolor","Blue")],binder)::
+ P.Mtext([None,"mathcolor","Blue"],binder)::
P.Mtext([],n ^ ":")::
(aux s)::
P.Mo([],".")::
(aux body)::tail)
| CE.Letin (xref,(n,s),body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
P.Mrow (attr,
P.Mtext([],("let "))::
P.Mtext([],(n ^ "="))::
P.Mtext([]," in ")::
(aux body)::tail)
| CE.Letrec (xref,defs,body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_defs =
(function
[] -> assert false
(P.Mtext([]," in ")::
(aux body)::tail))
| CE.Case (xref,a,np) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_patterns =
(function
[] -> []
if c > maxsize then
P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
(make_args_charcount ~tail:tail tl)
- else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([("width","0.2cm")]))::(make_args ~tail:tail l)))])]
+ else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
(*
function
CE.Symbol (xref,name,None,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow ([],P.Mi (attr,name)::tail)
| CE.Symbol (xref,name,Some subst,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
let rec make_subst =
(function
[] -> assert false
(make_subst subst)@
(P.Mtext([],"]")::tail))
| CE.LocalVar (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow ([],P.Mi (attr,name)::tail)
- | CE.Meta (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow ([],P.Mi (attr,name)::tail)
+ | CE.Meta (xref,name,l) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ 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 ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mn (attr,value)
else P.Mrow ([],P.Mn (attr,value)::tail)
| CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes ["helm:xref"] [axref] in
- let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
+ let aattr = make_attributes [Some "helm","xref"] [axref] in
+ let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
if (is_big t) then
(try
(let f = Hashtbl.find symbol_table_charcount n in
make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
else cexpr2pres t
| CE.Appl (xref,l) as t ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if (is_big t) then
P.Mtable (attr@P.standard_tbl_attr,
P.Mtr([],[P.Mtd([],P.Mrow([],
else cexpr2pres t
| CE.Binder (xref, kind,(n,s),body) as t ->
if (is_big t) then
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let binder =
if kind = "Lambda" then
Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
P.Mtable (attr@P.standard_tbl_attr,
[P.Mtr ([],[P.Mtd ([],
P.Mrow([],
- [P.Mtext([("mathcolor","Blue")],binder);
+ [P.Mtext([None,"mathcolor","Blue"],binder);
P.Mtext([],n ^ ":");
cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
P.Mtr ([],[P.Mtd ([],
else (cexpr2pres t ~tail:tail)
| CE.Letin (xref,(n,s),body) as t ->
if (is_big t) then
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
P.Mtable (attr@P.standard_tbl_attr,
[P.Mtr ([],[P.Mtd ([],
P.Mrow([],
- [P.Mtext([("mathcolor","Blue")],"let");
+ [P.Mtext([None,"mathcolor","Blue"],"let");
P.smallskip;
P.Mtext([],n ^ "=");
cexpr2pres_charcount s;
P.indented (cexpr2pres_charcount body))])])
else (cexpr2pres t)
| CE.Letrec (xref,defs,body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_defs =
(function
[] -> assert false
[P.Mtext([]," in ");
(aux body)])
| CE.Case (xref,a,np) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_patterns =
(function
[] -> []