some bug fixes

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 0309cf5930f757be60dcd3fb5aabb5a2e38f018d..150ec8de07c5d454ff7781e800ba1e9cb53ac89b 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -198,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
@@ -222,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
+   
+