]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
- cicInspect: relevant nodes count updated: letin nodes are not relevant
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index 3184aad369dc353383123c52121a14b7bc7cd0ed..6776bb1f3b04ae0b03fc9ec99f58ba58861e2512 100644 (file)
@@ -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
       | _            ->