X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=3b1e8d773294c963dabd001356b29e593dda661d;hb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;hp=62fcf03dfed5d0d80115eb3023f20708b81acad7;hpb=bb691187f8bbe22ec37ca41f9f3f42f9d8e505df;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 62fcf03df..3b1e8d773 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -37,12 +37,14 @@ type status = {
    helm_dir: string;
    heading_path: string;
    heading_lines: int;
-   package: string;
+   input_package: string;
+   output_package: string;
    input_base_uri: string;
    output_base_uri: string;
    input_path: string;
    output_path: string;
    script_ext: string;
+   coercions: (string * string) list;
    files: string list;
    requires: (string * string) list;
    scripts: script array
@@ -87,17 +89,21 @@ let init () =
    load_registry default_registry
 
 let make registry =
+   let id x = x in
+   let get_coercions = R.get_list (R.pair id id) in 
    load_registry registry;
    let st = {
       helm_dir = R.get_string "transcript.helm_dir";
       heading_path = R.get_string "transcript.heading_path";
       heading_lines = R.get_int "transcript.heading_lines";
-      package = R.get_string "package.name";
+      input_package = R.get_string "package.input_name";
+      output_package = R.get_string "package.output_name";
       input_base_uri = R.get_string "package.input_base_uri";
       output_base_uri = R.get_string "package.output_base_uri";
       input_path = R.get_string "package.input_path";
       output_path = R.get_string "package.output_path";
       script_ext = R.get_string "package.script_type";
+      coercions = get_coercions "package.coercion";
       files = [];
       requires = [];
       scripts = Array.make default_scripts default_script
@@ -133,7 +139,10 @@ let set_baseuri st name =
    
 let require st name inc =
    set_items st name [T.Include inc]
-   
+
+let get_coercion st str =
+   try List.assoc str st.coercions with Not_found -> ""
+
 let commit st name =
    let i = get_index st name in
    let script = st.scripts.(i) in
@@ -147,28 +156,33 @@ let commit st name =
    st.scripts.(i) <-  default_script
    
 let produce st =
-   let notation = st.package ^ "_notation" in
    let init name = set_heading st name; set_baseuri st name in
    let partition = function 
-      | T.Notation _ -> false
-      | _            -> true
+      | T.Coercion (false, _)
+      | T.Notation (false, _) -> false
+      | _                     -> true
    in
    let produce st name =
       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) -> 
+         | T.Inline (k, obj)   -> 
 	    let s = obj ^ G.string_of_inline_kind k in
 	    Some (T.Inline (k, Filename.concat in_base_uri s))
-	 | T.Include s       ->
+	 | T.Include s         ->
 	    begin 
 	       try Some (T.Include (List.assoc s st.requires))
 	       with Not_found -> None
 	    end
-	 | T.Coercion obj    ->
+	 | T.Coercion (b, obj) ->
+	    let str = get_coercion st obj in
+	    let base_uri = 
+	       if str <> "" then str else 
+	       if b then out_base_uri else in_base_uri
+	    in
 	    let s = obj ^ G.string_of_inline_kind T.Con in
-	    Some (T.Coercion (Filename.concat out_base_uri s))
-	 | item              -> Some item
+	    Some (T.Coercion (b, Filename.concat base_uri s))
+	 | item                -> Some item
       in
       Printf.eprintf "processing file name: %s ...\n" name; flush stderr; 
       let file = Filename.concat st.input_path (name ^ st.script_ext) in
@@ -181,10 +195,12 @@ let produce st =
 	 let local_items, global_items = List.partition partition items in
 	 let comment = T.Line (Printf.sprintf "From %s" name) in 
 	 if global_items <> [] then 
-	    set_items st notation (comment :: global_items);
-	 init name; require st name notation;
+	    set_items st st.input_package (comment :: global_items);
+	 init name; require st name st.input_package;
 	 set_items st name local_items; commit st name
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich 
    in
-   init notation; List.iter (produce st) st.files; commit st notation
+   init st.input_package; 
+   List.iter (produce st) st.files; 
+   commit st st.input_package