X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fmpresentation.ml;h=9ba9d848ebf674a3ff60ee39f44f2d0df518f892;hb=b41886e9d21d756279bd6a2ec3f19c17b1a64401;hp=34c65a4174e561f8fd42e9991b4588492f5e1360;hpb=ec350d553d0da4c2bdcf7504057ceb481217ac47;p=helm.git

diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml
index 34c65a417..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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\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"] (print_mpres pres))
+     ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres))
  >]