From: Claudio Sacerdoti Coen Date: Tue, 26 Sep 2006 11:36:36 +0000 (+0000) Subject: The precedence level is now an optional argument of the content to pres X-Git-Tag: make_still_working~6855 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7e217ef4d310903c23dd56a5943208edfeb9f20;p=helm.git The precedence level is now an optional argument of the content to pres transformation for terms. --- diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 308f23d22..297a52bc5 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -202,7 +202,7 @@ let add_parens child_prec child_assoc child_pos curr_prec t = end else t -let render ids_to_uris = +let render ids_to_uris ?(prec=(-1)) = let module A = Ast in let module P = Mpresentation in (* let use_unicode = true in *) @@ -418,7 +418,7 @@ let render ids_to_uris = in List.map boxify_pres (find_clusters terms) in - aux [] false (ref []) `Inner ~-1 + aux [] false (ref []) `Inner prec let rec print_box (t: boxml_markup) = Box.box2xml print_mpres t diff --git a/helm/software/components/content_pres/cicNotationPres.mli b/helm/software/components/content_pres/cicNotationPres.mli index 04411df2b..1d06d19ba 100644 --- a/helm/software/components/content_pres/cicNotationPres.mli +++ b/helm/software/components/content_pres/cicNotationPres.mli @@ -36,8 +36,10 @@ val box_of_mpres: mathml_markup -> boxml_markup (** {2 Rendering} *) (** level 1 -> level 0 - * @param ids_to_uris mapping id -> uri for hyperlinking *) -val render: (Cic.id, UriManager.uri) Hashtbl.t -> CicNotationPt.term -> markup + * @param ids_to_uris mapping id -> uri for hyperlinking + * @param prec precedence level *) +val render: + (Cic.id, UriManager.uri) Hashtbl.t -> ?prec:int -> CicNotationPt.term -> markup (** level 0 -> xml stream *) val print_xml: markup -> Xml.token Stream.t