X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=35f128a05b524078b117a394cb51b87a8554f6d1;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=1a092909e113cdafcd00343281d5b9192c2056b8;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 1a092909e..35f128a05 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -200,16 +200,17 @@ let add_parens child_prec curr_prec t = BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) -let render ids_to_uris ?(prec=(-1)) = +let lookup_uri ids_to_uris id = + try + let uri = Hashtbl.find ids_to_uris id in + Some (UriManager.string_of_uri uri) + with Not_found -> None +;; + +let render ~lookup_uri ?(prec=(-1)) = let module A = Ast in let module P = Mpresentation in (* let use_unicode = true in *) - let lookup_uri id = - (try - let uri = Hashtbl.find ids_to_uris id in - Some (UriManager.string_of_uri uri) - with Not_found -> None) - in let make_href xmlattrs xref = let xref_uris = List.fold_right