From 7782637e13656ec7d1d0ccc84e0d8cf894431187 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 19 Feb 2008 13:00:29 +0000
Subject: [PATCH] now inline "file.ma" is allowed. file.ma must be compiled and
 all its contents are inlined

---
 helm/software/components/library/librarian.ml |  9 ++++++-
 .../software/components/library/librarian.mli |  4 ++++
 helm/software/matita/applyTransformation.ml   | 24 +++++++++++++++----
 3 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 630cb4425..aa6b2e81d 100644
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -374,4 +374,11 @@ let write_deps_file root deps =
   close_out oc;
   HLog.message ("Generated: " ^ root ^ "/depends")
 ;;
- 
+
+(* FG ***********************************************************************)
+
+(* scheme uri part as defined in URI Generic Syntax (RFC 3986) *)
+let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:"
+
+let is_uri str =
+   Pcre.pmatch ~rex:uri_scheme_rex str
diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli
index f5698f2f4..e7b6df521 100644
--- a/helm/software/components/library/librarian.mli
+++ b/helm/software/components/library/librarian.mli
@@ -93,3 +93,7 @@ module Make :
 val load_deps_file: string -> (string * string list) list
 val write_deps_file: string -> (string * string list) list -> unit
 
+(* FG ***********************************************************************)
+
+(* true if the argunent starts with a uri scheme prefix *)
+val is_uri: string -> bool
diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 0309cf593..150ec8de0 100644
--- 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
+   
+    
-- 
2.39.2