X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcontent_pres%2FcicNotationPres.ml;h=308f23d22a13ea4826cde1050c8fbdc24a672c04;hb=b67ea513f11d1ef3d9fd228c64913561424662e2;hp=cc3a204a4e3874ba3ee55ccb3477932ae66447bc;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git diff --git a/helm/ocaml/content_pres/cicNotationPres.ml b/helm/ocaml/content_pres/cicNotationPres.ml index cc3a204a4..308f23d22 100644 --- a/helm/ocaml/content_pres/cicNotationPres.ml +++ b/helm/ocaml/content_pres/cicNotationPres.ml @@ -23,6 +23,10 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + +open Printf + module Ast = CicNotationPt module Mpres = Mpresentation @@ -175,31 +179,33 @@ 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 = let module A = Ast in let module P = Mpresentation in - let use_unicode = true in +(* let use_unicode = true in *) let lookup_uri id = (try let uri = Hashtbl.find ids_to_uris id in @@ -304,7 +310,7 @@ let render ids_to_uris = let new_xref = ref [] in let new_xmlattrs = ref [] in let new_pos = ref pos in - let reinit = ref false in +(* let reinit = ref false in *) let rec aux_attribute = function | A.AttributedTerm (attr, t) -> @@ -323,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