X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=ccf07423f6dd5cc14b5af35f6ede71356a5bbc2f;hb=0b76904a3f10bfd6390d26172fd6979626bd72f4;hp=120d31fdd3ffa2da105e152a96a7cd81c62c608d;hpb=d62f34ee8014169ba1e44669ab815b006780f454;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 120d31fdd..ccf07423f 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -27,7 +27,7 @@ module R  = Helm_registry
 module X  = HExtlib
 module T  = Types
 module G  = Grafite
-module HP = Http_getter
+module HG = Http_getter
 
 module O = Options
 
@@ -48,6 +48,7 @@ type status = {
    output_path: string;
    input_type: string;
    output_type: T.output_kind;
+   includes: (string * string) list;
    coercions: (string * string) list;
    files: string list;
    requires: (string * string) list;
@@ -94,11 +95,11 @@ let init () =
    let matita_registry = Filename.concat !O.cwd "matita" in
    load_registry default_registry;
    load_registry matita_registry;
-   HP.init ()
+   HG.init ()
 
 let make registry =
    let id x = x in
-   let get_coercions = R.get_list (R.pair id id) in 
+   let get_pairs = R.get_list (R.pair id id) in 
    let get_output_type key =
       match R.get_string key with
          | "procedural"  -> T.Procedural
@@ -117,7 +118,8 @@ let make registry =
       output_path = R.get_string "package.output_path";
       input_type = R.get_string "package.input_type";
       output_type = get_output_type "package.output_type";
-      coercions = get_coercions "package.coercion";
+      includes = get_pairs "package.include";
+      coercions = get_pairs "package.coercion";
       files = [];
       requires = [];
       scripts = Array.make default_scripts default_script
@@ -218,6 +220,10 @@ let produce st =
 	    path, Some item
 	 | item                         -> path, Some item
       in
+      let set_includes st name =
+      	 try require st name (List.assoc name st.includes) 
+	 with Not_found -> ()
+      in
       Printf.eprintf "processing file name: %s ...\n" name; flush stderr; 
       let file = Filename.concat st.input_path (name ^ st.input_type) in
       let ich = open_in file in
@@ -231,7 +237,7 @@ let produce st =
 	 let comment = T.Line (Printf.sprintf "From %s" name) in 
 	 if global_items <> [] then 
 	    set_items st st.input_package (comment :: global_items);
-	 init name; require st name st.input_package;
+	 init name; require st name st.input_package; set_includes st name;
 	 set_items st name local_items; commit st name
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich