]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/content_pres/cicNotationPres.ml
bugfix for missing parens: when the precedence does not change, parens are now added...
[helm.git] / helm / ocaml / content_pres / cicNotationPres.ml
index 6412c3f0c3138681fce1a178a19e11ed284bc5a3..308f23d22a13ea4826cde1050c8fbdc24a672c04 100644 (file)
@@ -25,6 +25,8 @@
 
 (* $Id$ *)
 
+open Printf
+
 module Ast = CicNotationPt
 module Mpres = Mpresentation
 
@@ -177,25 +179,27 @@ let is_atomic t =
   aux_mpres t
 
 let add_parens child_prec child_assoc child_pos curr_prec t =
+(*   eprintf
+    ("add_parens: " ^^
+    "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!")
+    child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
+    curr_prec; *)
   if is_atomic t then t
   else if child_prec >= 0
     && (child_prec < curr_prec
       || (child_prec = curr_prec &&
           child_assoc = Gramext.LeftA &&
-          child_pos = `Right)
+          child_pos <> `Left)
       || (child_prec = curr_prec &&
           child_assoc = Gramext.RightA &&
-          child_pos = `Left))
-  then  (* parens should be added *)
-(*     (prerr_endline "adding parens";
-    prerr_endline (Printf.sprintf "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d"
-      child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos
-      child_pos) curr_prec); *)
+          child_pos <> `Right))
+  then begin (* parens should be added *)
+(*     prerr_endline "adding parens!"; *)
     match t with
     | Mpresentation.Mobject (_, box) ->
         mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
     | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
-  else
+  end else
     t
 
 let render ids_to_uris =
@@ -325,9 +329,9 @@ let render ids_to_uris =
           | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
           | Some (child_prec, child_assoc) ->
               let t' = 
-                aux !new_xmlattrs mathonly new_xref !new_pos child_prec t
-              in
-              if !reset then t'
+                aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in
+              if !reset
+              then t'
               else add_parens child_prec child_assoc !new_pos prec t')
     in
     aux_attribute t