X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcontent_pres%2FcicNotationPres.ml;h=308f23d22a13ea4826cde1050c8fbdc24a672c04;hb=b67ea513f11d1ef3d9fd228c64913561424662e2;hp=6412c3f0c3138681fce1a178a19e11ed284bc5a3;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git diff --git a/helm/ocaml/content_pres/cicNotationPres.ml b/helm/ocaml/content_pres/cicNotationPres.ml index 6412c3f0c..308f23d22 100644 --- a/helm/ocaml/content_pres/cicNotationPres.ml +++ b/helm/ocaml/content_pres/cicNotationPres.ml @@ -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