X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=e0d62a8cb2ea24313dce951ecd4f7479aaad0dd2;hb=438a29376390222b94c1fe9772917c3aad50d42e;hp=92c3c73b469c8b9138e0aebf8cd2d3cec29cb43b;hpb=c5e25191f05bb2662fc738bfb2742eb03b941510;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 92c3c73b4..e0d62a8cb 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -24,10 +24,13 @@
  *)
 
 module R = Helm_registry
+module X = HExtlib
+module T = Types
+module G = Grafite
 
 type script = {
    name: string;
-   contents: Types.items
+   contents: T.items
 }
 
 type status = {
@@ -35,7 +38,8 @@ type status = {
    heading_path: string;
    heading_lines: int;
    package: string;
-   base_uri: string;
+   input_base_uri: string;
+   output_base_uri: string;
    input_path: string;
    output_path: string;
    script_ext: string;
@@ -89,7 +93,8 @@ let make registry =
       heading_path = R.get_string "transcript.heading_path";
       heading_lines = R.get_int "transcript.heading_lines";
       package = R.get_string "package.name";
-      base_uri = R.get_string "package.base_uri";
+      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";
@@ -120,11 +125,11 @@ let set_items st name items =
    
 let set_heading st name =
    let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in
-   set_items st name [Types.Heading heading] 
+   set_items st name [T.Heading heading] 
    
 let set_baseuri st name =
-   let baseuri = Filename.concat st.base_uri name in
-   set_items st name [Types.BaseUri baseuri]
+   let baseuri = Filename.concat st.output_base_uri name in
+   set_items st name [T.BaseUri baseuri]
    
 let commit st name =
    let i = get_index st name in
@@ -134,13 +139,25 @@ let commit st name =
    let cmd = Printf.sprintf "mkdir -p %s" path in
    let _ = Sys.command cmd in
    let och = open_out name in
-   Grafite.commit och script.contents;
+   G.commit och script.contents;
    close_out och;
    st.scripts.(i) <-  default_script
    
 let produce st =
    let init name = set_heading st name; set_baseuri st name in
+   let partition = function
+      | T.Coercion _ 
+      | T.Notation _ -> false
+      | _            -> true
+   in
    let produce st name =
+      let base_uri = Filename.concat st.input_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))
+	 | 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
       let ich = open_in file in
@@ -148,7 +165,12 @@ let produce st =
       try 
          let items = V8Parser.items V8Lexer.token lexbuf in
          close_in ich;
-         init name; set_items st name items; commit st name
+         let items = List.rev (X.list_rev_map_filter filter items) in
+	 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 st.package (comment :: global_items);
+	 init name; set_items st name local_items; commit st name
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich 
    in