(p,n,s)::(make_attributes (List.tl l1) tl)
;;
+let make_math_tail = List.map (fun s -> P.Mtext ([], s))
+
let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
let module CE = Content_expressions in
let module P = Mpresentation 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)
+ else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail))
| CE.Symbol (xref,name,Some subst,uri) ->
let attr =
make_attributes
P.Mi (attr,name)::
P.Mtext([],"[")::
(make_subst subst)@
- (P.Mtext([],"]")::tail))
+ (P.Mtext([],"]")::(make_math_tail tail)))
| CE.LocalVar (xref,name) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::tail)
+ else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail))
| CE.Meta (xref,name,l) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let l' =
P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
else
P.Mrow
- ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
+ ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail))
| CE.Num (xref,value) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mn (attr,value)
- else P.Mrow([],P.Mn (attr,value)::tail)
+ else P.Mrow([],P.Mn (attr,value)::(make_math_tail tail))
| CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
let aattr = make_attributes [Some "helm","xref"] [axref] in
let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
f tl ~priority ~assoc ~tail aattr sattr)
with notfound ->
P.Mrow(aattr,
- P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
+ P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::(make_math_tail tail))))
| CE.Appl (xref,l) as t ->
let attr = make_attributes [Some"helm","xref"] [xref] in
P.Mrow(attr,
- P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
+ P.Mo([],"(")::(make_args l)@(P.Mo([],")")::(make_math_tail tail)))
| CE.Binder (xref, kind,(n,s),body) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let binder =
P.Mtext([],n ^ ":")::
(aux s)::
P.Mo([],".")::
- (aux body)::tail)
+ (aux body)::(make_math_tail tail))
| CE.Letin (xref,(n,s),body) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
P.Mrow (attr,
P.Mtext([],(n ^ "="))::
(aux s)::
P.Mtext([]," in ")::
- (aux body)::tail)
+ (aux body)::(make_math_tail tail))
| CE.Letrec (xref,defs,body) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_defs =
P.Mtext([],("let rec "))::
(make_defs defs)@
(P.Mtext([]," in ")::
- (aux body)::tail))
+ (aux body)::(make_math_tail tail)))
| CE.Case (xref,a,np) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_patterns =
(aux a)::P.smallskip::
P.Mtext([],"with")::P.smallskip::
P.Mtext([],"[")::P.smallskip::
- (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::tail)) in
+ (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::(make_math_tail tail))) in
aux t
and
make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
- let module P = Mpresentation in
function
- [] -> tail
+ [] -> List.map (fun s -> P.Mtext ([], s)) tail
| a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
;;
+let make_box_tail = List.map (Box.b_text [])
+;;
+
let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
- let module P = Mpresentation in
function
[] -> []
- | [a] ->
- [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
+ | [a] -> [Box.indent (cexpr2pres_charcount ~tail:tail a)]
| (a::tl) as l ->
let c = List.fold_left countterm 0 l in
if c > maxsize then
- P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
+ (Box.indent (cexpr2pres_charcount a))::
(make_args_charcount ~tail:tail tl)
- else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
+ else
+ [Box.indent (Box.b_object (P.Mrow ([], (make_args ~tail:tail l))))]
(*
function
and
cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
- if not(is_big t) then (cexpr2pres ~priority ~assoc ~tail t)
+ if not (is_big t) then
+ Box.b_object (cexpr2pres ~priority ~assoc ~tail t)
else let aux = cexpr2pres_charcount in
match t with
CE.Symbol (xref,name,None,uri) ->
make_attributes
[Some "helm","xref";Some "xlink","href"] [xref;uri] in
if tail = [] then
- P.Mi (attr,name)
- else P.Mrow ([],P.Mi (attr,name)::tail)
+ Box.b_object (P.Mi (attr,name))
+ else
+ Box.b_h [] (Box.b_object (P.Mi (attr,name)) :: (make_box_tail tail))
| CE.Symbol (xref,name,Some subst,uri) ->
let attr =
make_attributes
(function
[] -> assert false
| [(uri,a)] ->
- [(cexpr2pres a);
- P.Mtext([],"/");
- P.Mi([],UriManager.name_of_uri uri)]
+ [Box.b_object (cexpr2pres a);
+ Box.b_text [] "/";
+ Box.b_object (P.Mi([],UriManager.name_of_uri uri))]
| (uri,a)::tl ->
- (cexpr2pres a)::
- P.Mtext([],"/")::
- P.Mi([],UriManager.name_of_uri uri)::
- P.Mtext([],"; ")::
- P.smallskip::
+ Box.b_object (cexpr2pres a) ::
+ Box.b_text [] "/" ::
+ Box.b_object (P.Mi([],UriManager.name_of_uri uri)) ::
+ Box.b_text [] "; " ::
+ Box.smallskip ::
(make_subst tl)) in
- P.Mrow ([],
- P.Mi (attr,name)::
- P.Mtext([],"[")::
+ Box.b_h [] (
+ Box.b_object (P.Mi (attr,name))::
+ Box.b_text [] "["::
(make_subst subst)@
- (P.Mtext([],"]")::tail))
+ (Box.b_text [] "]")::(make_box_tail tail) )
| CE.LocalVar (xref,name) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
- P.Mi (attr,name)
- else P.Mrow ([],P.Mi (attr,name)::tail)
+ Box.b_object (P.Mi (attr,name))
+ else
+ Box.b_object (P.Mrow ([], P.Mi (attr,name)::(make_math_tail tail)))
| CE.Meta (xref,name,l) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let l' =
| 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)
+ Box.b_object (P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail)))
| CE.Num (xref,value) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
- P.Mn (attr,value)
- else P.Mrow ([],P.Mn (attr,value)::tail)
+ Box.b_object (P.Mn (attr,value))
+ else
+ Box.b_object (P.Mrow ([], P.Mn (attr,value)::(make_math_tail tail)))
| CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
let aattr = make_attributes [Some "helm","xref"] [axref] in
let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
(let f = Hashtbl.find symbol_table_charcount n in
f tl ~priority ~assoc ~tail aattr sattr)
with notfound ->
- P.Mtable (aattr@P.standard_tbl_attr,
- P.Mtr([],[P.Mtd([],P.Mrow([],
- [P.Mtext([],"(");
- cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
- make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
+ Box.b_v aattr (
+ Box.b_h [] [
+ Box.b_text [] "(";
+ Box.b_object (cexpr2pres (CE.Symbol(sxref,n,subst,uri)))
+ ] ::
+ make_args_charcount ~tail:(")"::tail) tl
+ ))
| CE.Appl (xref,l) as t ->
let attr = make_attributes [Some "helm","xref"] [xref] in
- P.Mtable (attr@P.standard_tbl_attr,
- P.Mtr([],[P.Mtd([],P.Mrow([],
- [P.Mtext([],"(");
- cexpr2pres_charcount (List.hd l)]))])::
- make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
+ Box.b_v attr (
+ Box.b_h [] [
+ Box.b_text [] "(";
+ cexpr2pres_charcount (List.hd l)
+ ] ::
+ make_args_charcount ~tail:(")"::tail) (List.tl l)
+ )
| CE.Binder (xref, kind,(n,s),body) as t ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let binder =
else if kind = "Exists" then
Netconversion.ustring_of_uchar `Enc_utf8 0x2203
else "unknown" in
- P.Mtable (attr@P.standard_tbl_attr,
- [P.Mtr ([],[P.Mtd ([],
- P.Mrow([],
- [P.Mtext([None,"mathcolor","Blue"],binder);
- P.Mtext([],n ^ ":");
- cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
- P.Mtr ([],[P.Mtd ([],
- P.indented (cexpr2pres_charcount body ~tail:tail))])])
+ Box.b_v attr [
+ Box.b_h [] [
+ Box.b_text [None,"color","blue"] binder;
+ Box.b_text [] (n ^ ":");
+ cexpr2pres_charcount s ~tail:["."]
+ ];
+ Box.b_h [] [ Box.indent (cexpr2pres_charcount body ~tail:tail) ]
+ ]
| CE.Letin (xref,(n,s),body) as t ->
let attr = make_attributes [Some "helm","xref"] [xref] in
- P.Mtable (attr@P.standard_tbl_attr,
- [P.Mtr ([],[P.Mtd ([],
- P.Mrow([],
- [P.Mtext([None,"mathcolor","Blue"],"let");
- P.smallskip;
- P.Mtext([],n ^ "=");
- cexpr2pres_charcount s;
- P.smallskip;
- P.Mtext([],"in");
- ]))]);
- P.Mtr ([],[P.Mtd ([],
- P.indented (cexpr2pres_charcount body))])])
+ Box.b_v attr [
+ Box.b_h [] [
+ Box.b_kw "let";
+ Box.smallskip;
+ Box.b_text [] (n ^ "=");
+ cexpr2pres_charcount s;
+ Box.smallskip;
+ Box.b_kw "in"
+ ];
+ Box.indent (cexpr2pres_charcount body)
+ ]
| CE.Letrec (xref,defs,body) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_defs =
(function
[] -> assert false
| [(n,bo)] ->
- [P.Mtext([],(n ^ "="));(aux body)]
+ [Box.b_text [] (n ^ "="); (aux body)]
| (n,bo)::tl ->
- P.Mtext([],(n ^ "="))::
- (aux body)::P.Mtext([]," and")::(make_defs tl)) in
- P.Mrow (attr,
- P.Mtext([],("let rec "))::
- (make_defs defs)@
- [P.Mtext([]," in ");
- (aux body)])
+ Box.b_text [] (n ^ "=")::
+ (aux body)::
+ Box.smallskip::
+ Box.b_kw "and"::
+ (make_defs tl)) in
+ Box.b_h attr (
+ Box.b_kw "let" ::
+ Box.smallskip ::
+ Box.b_kw "rec" ::
+ Box.smallskip ::
+ make_defs defs @
+ [ Box.smallskip; Box.b_kw "in"; Box.smallskip; aux body ]
+ )
| CE.Case (xref,a,np) ->
let attr = make_attributes [Some "helm","xref"] [xref] in
let arg =
if (is_big a) then
- let tail = P.Mtext([],(" with"))::tail in
- [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]);
- P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])]
+ let tail = " with"::tail in (* LUCA: porcheria all'ennesima potenza, TODO ripensare il meccanismo del tail *)
+ [ Box.b_h [] [ Box.b_kw "match"; Box.smallskip ];
+ aux a ~tail
+ ]
else
- [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in
+ [ Box.b_h [] [
+ Box.b_kw "match";
+ Box.smallskip;
+ aux a ~tail;
+ Box.smallskip;
+ Box.b_kw "with"
+ ]
+ ] in
let rec make_patterns is_first ~tail =
function
[] -> []
| [(n,p)] ->
- let sep =
- if is_first then "[ " else "| " in
- [P.Mtr ([],
- [P.Mtd ([],
- make_pattern sep ~tail n p)])]
+ let sep = if is_first then "[ " else "| " in
+ [ Box.b_h [] [make_pattern sep ~tail n p] ]
| (n,p)::tl ->
let sep =
if is_first then "[ " else "| " in
- P.Mtr ([],
- [P.Mtd ([],
- make_pattern sep [] n p)])
- ::(make_patterns false ~tail tl)
+ [ Box.b_h [] ((make_pattern sep [] n p) :: (make_patterns false ~tail tl)) ]
and make_pattern sep ~tail n p =
let rec get_vars_and_body =
function
[] -> sep ^ n ^ " -> "
| l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
if (is_big body) then
- P.Mtable (P.standard_tbl_attr,
- [P.Mtr ([],
- [P.Mtd ([],P.Mtext([],lhs))]);
- P.Mtr ([],
- [P.Mtd ([],P.indented (aux ~tail body ))])])
+ Box.b_v [] [
+ Box.b_text [] lhs;
+ Box.indent (aux ~tail body)
+ ]
else
- P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in
+ Box.b_h [] [ Box.b_text [] lhs; aux ~tail body ]
+ in
let patterns =
- make_patterns true np ~tail:(P.Mtext([],"]")::tail) in
- P.Mtable (attr@P.standard_tbl_attr,
- arg@patterns)
+ make_patterns true np ~tail:("]"::tail) in
+ Box.b_v attr (arg@patterns)
;;
projects / helm.git / blobdiff