]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
- Procedural convertible rewrites in the conclusion are now detected and replaced...
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index 6776bb1f3b04ae0b03fc9ec99f58ba58861e2512..a51d3f0c2bd9df07bd5d769a3b083dc18ea793a4 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 src inc =
-   set_items st name [T.Include (src, inc)]
+let require st name moo inc =
+   set_items st name [T.Include (moo, inc)]
 
 let get_coercion st str =
    try List.assoc str st.coercions with Not_found -> ""
@@ -198,6 +198,8 @@ let make_script_name st script name =
 let get_iparams st name =
    let map = function
       | "nodefaults" -> GA.IPNoDefaults
+      | "coercions"  -> GA.IPCoercions
+      | "comments"   -> GA.IPComments
       | s            -> failwith ("unknown inline parameter: " ^ s)
    in
    List.map map (X.list_assoc_all name st.iparams) 
@@ -233,14 +235,19 @@ let produce st =
            let obj, p = 
               if b then Filename.concat (make_path path) obj, make_prefix path
               else obj, p
-           in 
-           let s = obj ^ G.string_of_inline_kind k in
-           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 (src, s)           ->
+           in
+           let ext = G.string_of_inline_kind k in
+           let s = Filename.concat in_base_uri (obj ^ ext) in
+           let params = 
+              params @
+              get_iparams st "*" @
+              get_iparams st ("*" ^ ext) @
+              get_iparams st (Filename.concat name obj)
+           in
+           path, Some (T.Inline (b, k, s, p, f, params))
+        | T.Include (moo, s)           ->
            begin 
-              try path, Some (T.Include (src, List.assoc s st.requires))
+              try path, Some (T.Include (moo, List.assoc s st.requires))
               with Not_found -> path, None
            end
         | T.Coercion (b, obj)          ->
@@ -258,7 +265,7 @@ let produce st =
         | item                         -> path, Some item
       in
       let set_includes st name =
-        try require st name false (List.assoc name st.includes) 
+        try require st name true (List.assoc name st.includes) 
         with Not_found -> ()
       in
       let rec remove_lines ich n =
@@ -279,8 +286,8 @@ 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 true file
-           | _            -> require st name true st.input_package
+           | T.Grafite "" -> require st name false file
+           | _            -> require st name false st.input_package
         end; 
         set_includes st name; set_items st name local_items; commit st name
       with e -> 
@@ -293,7 +300,7 @@ let produce st =
          List.iter (produce st) st.files
       | T.Grafite s  ->
          let theory = Filename.concat st.input_path s in
-        require st st.input_package true theory;
+        require st st.input_package false theory;
          List.iter (produce st) st.files;
          commit st st.input_package
       | _            ->