]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
* the transformations have been ported so to generate BoxML + MathML
[helm.git] / helm / ocaml / cic_transformations / cexpr2pres_hashtbl.ml
index 79c9943c9985fc3b9839a3aa823a10e2701d2eba..7cb3ba13c132cfddae7870e361c95119dede13dd 100644 (file)
@@ -47,32 +47,60 @@ let unary f =
   | _ -> assert false
 ;;
 
+let m_open_fence = P.Mtext([], "(")
+let b_open_fence = Box.b_text [] "("
+(*
+let m_close_fence = P.Mtext([], ")")
+let b_close_fence = Box.b_text [] ")"
+*)
+
+let b_h_with_open_fence attrs a b op =
+  Box.b_h attrs [ b_open_fence; a; Box.b_object op; b ]
+let b_h_without_open_fence attrs a b op =
+  Box.b_h attrs [ a; Box.b_object op; b ]
+let b_v_with_open_fence attrs a b op =
+  Box.b_v attrs [
+    Box.b_h [] [ b_open_fence; a];
+    Box.b_indent (Box.b_h [] [ Box.b_object op; b ])
+  ]
+let b_v_without_open_fence attrs a b op =
+  Box.b_v attrs [
+    a;
+    Box.b_indent (Box.b_h [] [ Box.b_object op; b ])
+  ]
+
+let m_row_with_open_fence = P.row_with_brackets
+let m_row_without_open_fence = P.row_without_brackets
+
+let m_close_fence = ")"
+let b_close_fence = ")"
+
 let init
  ~(cexpr2pres:
    ?priority:int ->
    ?assoc:bool ->
-   ?tail:Mpresentation.mpres list ->
+   ?tail:string list ->
    Content_expressions.cexpr -> 
    Mpresentation.mpres)
  ~(cexpr2pres_charcount:
    ?priority:int ->
    ?assoc:bool ->
-   ?tail:Mpresentation.mpres list ->
+   ?tail:string list ->
    Content_expressions.cexpr -> 
-   Mpresentation.mpres)
+   Mpresentation.mpres Box.box)
 =
 
 (* arrow *)
 Hashtbl.add C2P.symbol_table "arrow" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 5) || (priority = 5 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
          (cexpr2pres ~priority:5 ~assoc:true 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:((m_close_fence)::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
          (cexpr2pres ~priority:5 ~assoc:true ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
@@ -80,13 +108,13 @@ Hashtbl.add C2P.symbol_table "arrow" (binary
 Hashtbl.add C2P.symbol_table_charcount "arrow" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:true 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:[] a)
          (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
@@ -95,13 +123,13 @@ Hashtbl.add C2P.symbol_table_charcount "arrow" (binary
 Hashtbl.add C2P.symbol_table "eq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,"="))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"="))));
@@ -109,13 +137,13 @@ Hashtbl.add C2P.symbol_table "eq" (binary
 Hashtbl.add C2P.symbol_table_charcount "eq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,"="))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"="))));
@@ -124,13 +152,13 @@ Hashtbl.add C2P.symbol_table_charcount "eq" (binary
 Hashtbl.add C2P.symbol_table "and" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 20) || (priority = 20 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:20 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:20 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
@@ -138,13 +166,13 @@ Hashtbl.add C2P.symbol_table "and" (binary
 Hashtbl.add C2P.symbol_table_charcount "and" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 20) || (priority = 20 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:20 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:20 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
@@ -153,13 +181,13 @@ Hashtbl.add C2P.symbol_table_charcount "and" (binary
 Hashtbl.add C2P.symbol_table "or" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 10) || (priority = 10 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:10 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:10 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
@@ -167,13 +195,13 @@ Hashtbl.add C2P.symbol_table "or" (binary
 Hashtbl.add C2P.symbol_table_charcount "or" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 10) || (priority = 10 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:10 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:10 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
@@ -182,13 +210,13 @@ Hashtbl.add C2P.symbol_table_charcount "or" (binary
 Hashtbl.add C2P.symbol_table "iff" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 5) || (priority = 5 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:5 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:5 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
@@ -196,13 +224,13 @@ Hashtbl.add C2P.symbol_table "iff" (binary
 Hashtbl.add C2P.symbol_table_charcount "iff" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 5) || (priority = 5 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:5 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
@@ -210,18 +238,18 @@ Hashtbl.add C2P.symbol_table_charcount "iff" (binary
 (* not *)
 Hashtbl.add C2P.symbol_table "not" (unary
   (fun a ~priority ~assoc ~tail attr sattr ->
-     P.Mrow([],[
-       P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
-       cexpr2pres a;P.Mtext([],")")])));
+     (P.Mrow([], [
+       m_open_fence; P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
+       cexpr2pres a; P.Mtext ([], m_close_fence)])))) ;
 
 (* inv *)
 Hashtbl.add C2P.symbol_table "inv" (unary
   (fun a ~priority ~assoc ~tail attr sattr ->
     P.Msup([],
       P.Mrow([],[
-        P.Mtext([],"(");
+        m_open_fence;
         cexpr2pres a;
-        P.Mtext([],")")]),
+        P.Mtext ([], m_close_fence)]),
       P.Mrow([],[
         P.Mo([],"-");
         P.Mn([],"1")]))));
@@ -231,21 +259,21 @@ Hashtbl.add C2P.symbol_table "opp" (unary
   (fun a ~priority ~assoc ~tail attr sattr ->
     P.Mrow([],[
       P.Mo([],"-");
-      P.Mtext([],"(");
+      m_open_fence;
       cexpr2pres a;
-      P.Mtext([],")")])));
+      P.Mtext ([], m_close_fence)])));
 
 (* leq *)
 Hashtbl.add C2P.symbol_table "leq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
@@ -253,13 +281,13 @@ Hashtbl.add C2P.symbol_table "leq" (binary
 Hashtbl.add C2P.symbol_table_charcount "leq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
@@ -268,13 +296,13 @@ Hashtbl.add C2P.symbol_table_charcount "leq" (binary
 Hashtbl.add C2P.symbol_table "lt" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,"<"))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"<"))));
@@ -282,13 +310,13 @@ Hashtbl.add C2P.symbol_table "lt" (binary
 Hashtbl.add C2P.symbol_table_charcount "lt" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,"<"))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
@@ -297,13 +325,13 @@ Hashtbl.add C2P.symbol_table_charcount "lt" (binary
 Hashtbl.add C2P.symbol_table "geq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
@@ -311,13 +339,13 @@ Hashtbl.add C2P.symbol_table "geq" (binary
 Hashtbl.add C2P.symbol_table_charcount "geq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
@@ -326,13 +354,13 @@ Hashtbl.add C2P.symbol_table_charcount "geq" (binary
 Hashtbl.add C2P.symbol_table "gt" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,">"))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,">"))));
@@ -340,13 +368,13 @@ Hashtbl.add C2P.symbol_table "gt" (binary
 Hashtbl.add C2P.symbol_table_charcount "gt" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 40) || (priority = 40 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,">"))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,">"))));
@@ -355,13 +383,13 @@ Hashtbl.add C2P.symbol_table_charcount "gt" (binary
 Hashtbl.add C2P.symbol_table "plus" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 60) || (priority = 60 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:60 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,"+"))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"+"))));
@@ -369,13 +397,13 @@ Hashtbl.add C2P.symbol_table "plus" (binary
 Hashtbl.add C2P.symbol_table_charcount "plus" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 60) || (priority = 60 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,"+"))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"+"))));
@@ -384,13 +412,13 @@ Hashtbl.add C2P.symbol_table_charcount "plus" (binary
 Hashtbl.add C2P.symbol_table "times" (binary 
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 70) || (priority = 70 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:70 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,"*"))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"*"))));
@@ -398,13 +426,13 @@ Hashtbl.add C2P.symbol_table "times" (binary
 Hashtbl.add C2P.symbol_table_charcount "times" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 70) || (priority = 70 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:70 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,"*"))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"*"))));
@@ -413,13 +441,13 @@ Hashtbl.add C2P.symbol_table_charcount "times" (binary
 Hashtbl.add C2P.symbol_table "minus" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 60) || (priority = 60 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:60 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,"-"))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"-"))));
@@ -427,13 +455,13 @@ Hashtbl.add C2P.symbol_table "minus" (binary
 Hashtbl.add C2P.symbol_table_charcount "minus" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 60) || (priority = 60 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,"-"))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"-"))));
@@ -442,13 +470,13 @@ Hashtbl.add C2P.symbol_table_charcount "minus" (binary
 Hashtbl.add C2P.symbol_table "div" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 60) || (priority = 60 && assoc) then
-       P.row_with_brackets aattr
+       m_row_with_open_fence aattr
          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:60 ~assoc:false 
-            ~tail:(P.Mtext([],")")::tail) b)
+            ~tail:(m_close_fence::tail) b)
          (P.Mo(sattr,"/"))
      else 
-       P.row_without_brackets aattr
+       m_row_without_open_fence aattr
          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"/"))));
@@ -456,13 +484,13 @@ Hashtbl.add C2P.symbol_table "div" (binary
 Hashtbl.add C2P.symbol_table_charcount "div" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
      if (priority > 60) || (priority = 60 && assoc) then
-       P.two_rows_table_with_brackets aattr
+       b_v_with_open_fence aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false 
-           ~tail:(P.Mtext([],")")::tail) b)
+           ~tail:(b_close_fence::tail) b)
          (P.Mo(sattr,"/"))
      else
-       P.two_rows_table_without_brackets aattr
+       b_v_without_open_fence aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
          (P.Mo(sattr,"/"))))