From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 19 Feb 2008 13:00:29 +0000 (+0000)
Subject: now inline "file.ma" is allowed.
X-Git-Tag: make_still_working~5597
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7782637e13656ec7d1d0ccc84e0d8cf894431187;p=helm.git

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 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
+   
+