X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=8908897dd3017684192f90736d83280981cee3ea;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=e0d62a8cb2ea24313dce951ecd4f7479aaad0dd2;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index e0d62a8cb..8908897dd 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -131,6 +131,9 @@ let set_baseuri st name =
    let baseuri = Filename.concat st.output_base_uri name in
    set_items st name [T.BaseUri baseuri]
    
+let require st name =
+   set_items st name [T.Include st.package]
+   
 let commit st name =
    let i = get_index st name in
    let script = st.scripts.(i) in
@@ -145,17 +148,25 @@ let commit st name =
    
 let produce st =
    let init name = set_heading st name; set_baseuri st name in
-   let partition = function
-      | T.Coercion _ 
+   let partition = function 
       | T.Notation _ -> false
       | _            -> true
    in
    let produce st name =
-      let base_uri = Filename.concat st.input_base_uri name in
+      let in_base_uri = Filename.concat st.input_base_uri name in
+      let out_base_uri = Filename.concat st.output_base_uri name in
       let filter = function
          | T.Inline (k, obj) -> 
 	    let s = obj ^ G.string_of_inline_kind k in
-	    Some (T.Inline (k, Filename.concat base_uri s))
+	    Some (T.Inline (k, Filename.concat in_base_uri s))
+	 | T.Include s       ->
+	    begin 
+	       try Some (T.Include (List.assoc s st.requires))
+	       with Not_found -> None
+	    end
+	 | T.Coercion obj    ->
+	    let s = obj ^ G.string_of_inline_kind T.Con in
+	    Some (T.Coercion (Filename.concat out_base_uri s))
 	 | item              -> Some item
       in
       Printf.eprintf "processing file name: %s ...\n" name; flush stderr; 
@@ -170,7 +181,8 @@ let produce st =
 	 let comment = T.Line (Printf.sprintf "From %s" name) in 
 	 if global_items <> [] then 
 	    set_items st st.package (comment :: global_items);
-	 init name; set_items st name local_items; commit st name
+	 init name; require st name;
+	 set_items st name local_items; commit st name
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich 
    in