X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=150ec8de07c5d454ff7781e800ba1e9cb53ac89b;hb=10d3194c1b42dfa72e51000ff2cc217f937b43ac;hp=19a40960774ff0ad6a4c6bbc00d28e58bf692321;hpb=397b5f9d848e63a9703a1f90faf9869092ec8893;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 19a409607..150ec8de0 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -48,8 +48,7 @@ let mml_of_cic_sequent metasenv sequent =
   in
   let content_sequent = Acic2content.map_sequent asequent in 
   let pres_sequent = 
-    (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
-  in
+   Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in
   let xmlpres = mpres_document pres_sequent in
   (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
    unsh_sequent,
@@ -86,20 +85,23 @@ let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
   BoxPp.render_to_string ~map_unicode_to_tex
     (function x::_ -> x | _ -> assert false) size pres_sequent
 
-let txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv sequent =
+let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
+ metasenv sequent =
   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
     Cic2acic.asequent_of_sequent metasenv sequent 
   in
   let _,_,_,t = Acic2content.map_sequent asequent in 
-  let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
+  let t, ids_to_uris =
+   TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
   let t = TermContentPres.pp_ast t in
   let t = CicNotationPres.render ids_to_uris t in
   BoxPp.render_to_string ~map_unicode_to_tex
     (function x::_ -> x | _ -> assert false) size t
 
 let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = 
-  let fake_sequent = (-1,context,t) in
-  txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv fake_sequent 
+ let fake_sequent = (-1,context,t) in
+  txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size
+   metasenv fake_sequent 
 ;;
 
 ignore (
@@ -148,14 +150,11 @@ let remove_closed_substs s =
 
 let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = 
    let ast, ids_to_uris = 
-      TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
-   in
+    TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
    let bobj =
       CicNotationPres.box_of_mpres (
          CicNotationPres.render ~prec:90 ids_to_uris 
-            (TermContentPres.pp_ast ast)
-      )
-   in
+            (TermContentPres.pp_ast ast)) in
    let render = function _::x::_ -> x | _ -> assert false in
    let mpres = CicNotationPres.mpres_of_box bobj in
    let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
@@ -199,12 +198,13 @@ let txt_of_cic_object
         let aux = GrafiteAstPp.pp_statement
          ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
         let script = 
-    Acic2Procedural.acic2procedural 
-           ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj 
+           Acic2Procedural.acic2procedural 
+              ~ids_to_inner_sorts ~ids_to_inner_types 
+	      ?depth ?skip_thm_and_qed prefix aobj 
   in
-        String.concat "" (List.map aux script) ^ "\n\n"
+        "\n\n" ^ String.concat "" (List.map aux script)
 
-let txt_of_inline_macro ~map_unicode_to_tex style suri prefix =
+let txt_of_inline_uri ~map_unicode_to_tex style suri prefix =
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
            Printexc.to_string e ^ " " ^ Lazy.force s
@@ -223,3 +223,18 @@ let txt_of_inline_macro ~map_unicode_to_tex style suri prefix =
             (UriManager.string_of_uri uri) (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)
+
+let txt_of_inline_macro ~map_unicode_to_tex style name prefix =
+   let suri = 
+      if Librarian.is_uri name then name else
+      let include_paths = 
+         Helm_registry.get_list Helm_registry.string "matita.includes"
+      in
+      let _, baseuri, _, _ = 
+         Librarian.baseuri_of_script ~include_paths name
+      in
+      baseuri
+   in
+   txt_of_inline_uri ~map_unicode_to_tex style suri prefix
+   
+