X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=6776bb1f3b04ae0b03fc9ec99f58ba58861e2512;hb=d17a38ddca548c784e9efa7c55e87c80203b024d;hp=3184aad369dc353383123c52121a14b7bc7cd0ed;hpb=b378b7f4f2a3a897c4b69f44d4d1d54cc4d0aa56;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 3184aad36..6776bb1f3 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -179,8 +179,8 @@ let set_heading st name =
    let heading = st.heading_path, st.heading_lines in
    set_items st name [T.Heading heading] 
    
-let require st name inc =
-   set_items st name [T.Include inc]
+let require st name src inc =
+   set_items st name [T.Include (src, inc)]
 
 let get_coercion st str =
    try List.assoc str st.coercions with Not_found -> ""
@@ -238,9 +238,9 @@ let produce st =
 	    let full_s = Filename.concat in_base_uri s in
 	    let params = params @ get_iparams st (Filename.concat name obj) in
 	    path, Some (T.Inline (b, k, full_s, p, f, params))
-	 | T.Include s                  ->
+	 | T.Include (src, s)           ->
 	    begin 
-	       try path, Some (T.Include (List.assoc s st.requires))
+	       try path, Some (T.Include (src, List.assoc s st.requires))
 	       with Not_found -> path, None
 	    end
 	 | T.Coercion (b, obj)          ->
@@ -258,7 +258,7 @@ let produce st =
 	 | item                         -> path, Some item
       in
       let set_includes st name =
-      	 try require st name (List.assoc name st.includes) 
+      	 try require st name false (List.assoc name st.includes) 
 	 with Not_found -> ()
       in
       let rec remove_lines ich n =
@@ -279,21 +279,21 @@ let produce st =
 	    set_items st st.input_package (comment :: global_items);
 	 init name; 
 	 begin match st.input_type with
-	    | T.Grafite "" -> require st name file
-	    | _            -> require st name st.input_package
+	    | T.Grafite "" -> require st name true file
+	    | _            -> require st name true st.input_package
 	 end; 
 	 set_includes st name; set_items st name local_items; commit st name
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich 
    in
    is_ma st st.input_package;
-   init st.input_package; require st st.input_package "preamble"; 
+   init st.input_package; require st st.input_package false "preamble"; 
    match st.input_type with
       | T.Grafite "" ->
          List.iter (produce st) st.files
       | T.Grafite s  ->
          let theory = Filename.concat st.input_path s in
-	 require st st.input_package theory;
+	 require st st.input_package true theory;
          List.iter (produce st) st.files;
          commit st st.input_package
       | _            ->