now inline "file.ma" is allowed.

file.ma must be compiled and all its contents are inlined

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 630cb44258eb2f6593039dfbf7cea0dd11fa4687..aa6b2e81dd2e3997f96d41669e7ff245fc50e306 100644 (file)
--- 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 f5698f2f476f03725e08c6c3767b9d3539b5f31c..e7b6df521aaff07fe08b57d1fa2be9eabbdcf90d 100644 (file)
--- 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 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
+   
+