X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fmpresentation.ml;h=9ba9d848ebf674a3ff60ee39f44f2d0df518f892;hb=b41886e9d21d756279bd6a2ec3f19c17b1a64401;hp=09eb6331e085caa2dd1ae94a506ecdd16b4f8beb;hpb=ab06d9617b863a42a49f9a407694a9605f500b98;p=helm.git diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 09eb6331e..9ba9d848e 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -73,8 +73,8 @@ and mtd = Mtd of attr * mpres and attr = (string option * string * string) list ;; -let smallskip = Mspace([None,"width","0.1cm"]);; -let indentation = Mspace([None,"width","0.3cm"]);; +let smallskip = Mspace([None,"width","0.5em"]);; +let indentation = Mspace([None,"width","1em"]);; let indented elem = Mrow([],[indentation;elem]);; @@ -102,7 +102,7 @@ let two_rows_table_without_brackets attr a b op = 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;op;b]) + Mrow(attr,[Mtext([],"(");a;op;b;Mtext([],")")]) let row_without_brackets attr a b op = Mrow(attr,[a;op;b]) @@ -207,17 +207,17 @@ and print_mrow = and print_mtd = let module X = Xml in function - Mtd (attr,m) -> X.xml_nempty ~prefix "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 = +let document_of_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" - ] (print_mpres pres) + ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres)) >]