X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fmpresentation.ml;h=3c4f929024b080b311b2abd36898768e3946ec58;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=116b845b5f358f830acecd741b369ec229f771a5;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 116b845b5..3c4f92902 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -66,28 +66,22 @@ type (* Enlivening Expressions *) | Maction of attr * mpres list -and +and row = Mtr of attr * mtd list - row = Mtr of attr * mtd list - -and - - mtd = Mtd of attr * mpres - -and - - attr = (string * string) list +and mtd = Mtd of attr * mpres +and attr = (string option * string * string) list ;; -let smallskip = Mspace([("width","0.1cm")]);; -let indentation = Mspace([("width","0.3cm")]);; +let smallskip = Mspace([None,"width","0.1cm"]);; +let indentation = Mspace([None,"width","0.3cm"]);; let indented elem = Mrow([],[indentation;elem]);; let standard_tbl_attr = - [("align","baseline 1");("equalrows","false");("columnalign","left")];; + [None,"align","baseline 1";None,"equalrows","false";None,"columnalign","left"] +;; let two_rows_table attr a b = Mtable(attr@standard_tbl_attr, @@ -98,91 +92,94 @@ let two_rows_table_with_brackets attr a b op = (* only the open bracket is added; the closed bracket must be in b *) Mtable(attr@standard_tbl_attr, [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]); - Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);; + Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);; let two_rows_table_without_brackets attr a b op = Mtable(attr@standard_tbl_attr, [Mtr([],[Mtd([],a)]); - Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);; + Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);; let row_with_brackets attr a b op = (* by analogy with two_rows_table_with_brackets we only add the open brackets *) - Mrow(attr,[Mtext([],"(");a;smallskip;op;smallskip;b]) + Mrow(attr,[Mtext([],"(");a;op;b]) let row_without_brackets attr a b op = - Mrow(attr,[a;smallskip;op;smallskip;b]) + Mrow(attr,[a;op;b]) + +(* MathML prefix *) +let prefix = "m";; let rec print_mpres = let module X = Xml in - function - Mi (attr,s) -> X.xml_nempty "mi" attr (X.xml_cdata s) - | Mn (attr,s) -> X.xml_nempty "mn" attr (X.xml_cdata s) - | Mo (attr,s) -> X.xml_nempty "mo" attr (X.xml_cdata s) - | Mtext (attr,s) -> X.xml_nempty "mtext" attr (X.xml_cdata s) - | Mspace attr -> X.xml_empty "mspace" attr - | Ms (attr,s) -> X.xml_nempty "ms" attr (X.xml_cdata s) - | Mgliph (attr,s) -> X.xml_nempty "mgliph" attr (X.xml_cdata s) + function + Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s) + | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s) + | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s) + | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s) + | Mspace attr -> X.xml_empty ~prefix "mspace" attr + | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s) + | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s) (* General Layout Schemata *) | Mrow (attr,l) -> - X.xml_nempty "mrow" attr + X.xml_nempty ~prefix "mrow" attr [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) >] | Mfrac (attr,m1,m2) -> - X.xml_nempty "mfrac" attr + X.xml_nempty ~prefix "mfrac" attr [< print_mpres m1; print_mpres m2 >] | Msqrt (attr,m) -> - X.xml_nempty "msqrt" attr [< print_mpres m >] + X.xml_nempty ~prefix "msqrt" attr [< print_mpres m >] | Mroot (attr,m1,m2) -> - X.xml_nempty "mroot" attr + X.xml_nempty ~prefix "mroot" attr [< print_mpres m1; print_mpres m2 >] | Mstyle (attr,m) -> - X.xml_nempty "mstyle" attr [< print_mpres m >] + X.xml_nempty ~prefix "mstyle" attr [< print_mpres m >] | Merror (attr,m) -> - X.xml_nempty "merror" attr [< print_mpres m >] + X.xml_nempty ~prefix "merror" attr [< print_mpres m >] | Mpadded (attr,m) -> - X.xml_nempty "mpadded" attr [< print_mpres m >] + X.xml_nempty ~prefix "mpadded" attr [< print_mpres m >] | Mphantom (attr,m) -> - X.xml_nempty "mphantom" attr [< print_mpres m >] + X.xml_nempty ~prefix "mphantom" attr [< print_mpres m >] | Mfenced (attr,l) -> - X.xml_nempty "mfenced" attr + X.xml_nempty ~prefix "mfenced" attr [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) >] | Menclose (attr,m) -> - X.xml_nempty "menclose" attr [< print_mpres m >] + X.xml_nempty ~prefix "menclose" attr [< print_mpres m >] (* Script and Limit Schemata *) | Msub (attr,m1,m2) -> - X.xml_nempty "msub" attr + X.xml_nempty ~prefix "msub" attr [< print_mpres m1; print_mpres m2 >] | Msup (attr,m1,m2) -> - X.xml_nempty "msup" attr + X.xml_nempty ~prefix "msup" attr [< print_mpres m1; print_mpres m2 >] | Msubsup (attr,m1,m2,m3) -> - X.xml_nempty "msubsup" attr + X.xml_nempty ~prefix "msubsup" attr [< print_mpres m1; print_mpres m2; print_mpres m3 >] | Munder (attr,m1,m2) -> - X.xml_nempty "munder" attr + X.xml_nempty ~prefix "munder" attr [< print_mpres m1; print_mpres m2 >] | Mover (attr,m1,m2) -> - X.xml_nempty "mover" attr + X.xml_nempty ~prefix "mover" attr [< print_mpres m1; print_mpres m2 >] | Munderover (attr,m1,m2,m3) -> - X.xml_nempty "munderover" attr + X.xml_nempty ~prefix "munderover" attr [< print_mpres m1; print_mpres m2; print_mpres m3 @@ -190,12 +187,12 @@ let rec print_mpres = (* | Multiscripts of ??? NOT IMPLEMEMENTED *) (* Tables and Matrices *) | Mtable (attr, rl) -> - X.xml_nempty "mtable" attr + X.xml_nempty ~prefix "mtable" attr [< (List.fold_right (fun x i -> [< (print_mrow x) ; i >]) rl [<>]) >] (* Enlivening Expressions *) | Maction (attr, l) -> - X.xml_nempty "maction" attr + X.xml_nempty ~prefix "maction" attr [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) >] @@ -203,16 +200,24 @@ and print_mrow = let module X = Xml in function Mtr (attr, l) -> - X.xml_nempty "mtr" attr + X.xml_nempty ~prefix "mtr" attr [< (List.fold_right (fun x i -> [< (print_mtd x) ; i >]) l [<>]) >] and print_mtd = let module X = Xml in function - Mtd (attr,m) -> X.xml_nempty "mtd" attr (print_mpres m) + Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr [< (print_mpres m) ; X.xml_nempty ~prefix "mphantom" [] (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >] ;; - +let print_mpres pres = + [< Xml.xml_cdata "\n" ; + Xml.xml_cdata "\n"; + Xml.xml_nempty ~prefix "math" + [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; + Some "xmlns","helm","http://www.cs.unibo.it/helm" ; + Some "xmlns","xlink","http://www.w3.org/1999/xlink" + ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres)) + >]