X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=282cfe26ee1655329ab3600802211bc020f6dcf9;hb=be2a030746e20744f9a317a31c7053bcfbb6e505;hp=46f53d8860c85a00ac600373c36e63b5f74dbfa9;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 46f53d886..282cfe26e 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -929,7 +929,7 @@ let joint_def2pres term2pres def =
   | `Inductive ind -> inductive2pres term2pres ind
   | _ -> assert false (* ZACK or raise ToDo? *)
 
-let content2pres 
+let content2pres0
   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
   (id,params,metasenv,obj) 
 =
@@ -976,7 +976,7 @@ let content2pres
 let content2pres 
   ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts 
 =
-  content2pres ?skip_initial_lambdas ?skip_thm_and_qed
+  content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
        TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
@@ -985,3 +985,15 @@ let content2pres
         (CicNotationPres.render
           ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
           (TermContentPres.pp_ast ast)))
+
+let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
+ let lookup_uri id =
+  try
+   let nref = Hashtbl.find ids_to_nrefs id in
+    Some (NReference.string_of_reference nref)
+  with Not_found -> None
+ in
+  content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+    (fun ?(prec=90) ast ->
+      CicNotationPres.box_of_mpres
+       (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))