X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2Fengine.ml;h=66c6c33be85a2b53e16352a7c41b57e77ee2a8d0;hb=b44a732a930584aa08f4a78371dd9ac5b405f31e;hp=3b1e8d773294c963dabd001356b29e593dda661d;hpb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;p=helm.git

diff --git a/components/binaries/transcript/engine.ml b/components/binaries/transcript/engine.ml
index 3b1e8d773..66c6c33be 100644
--- a/components/binaries/transcript/engine.ml
+++ b/components/binaries/transcript/engine.ml
@@ -143,6 +143,12 @@ let require st name inc =
 let get_coercion st str =
    try List.assoc str st.coercions with Not_found -> ""
 
+let make_path path =
+   List.fold_left Filename.concat "" (List.rev path)
+
+let make_prefix path =
+   String.concat "__" (List.rev path) ^ "__"
+
 let commit st name =
    let i = get_index st name in
    let script = st.scripts.(i) in
@@ -165,24 +171,29 @@ let produce st =
    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)   -> 
+      let filter path = function
+         | T.Inline (b, k, obj, p)      -> 
+	    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
-	    Some (T.Inline (k, Filename.concat in_base_uri s))
-	 | T.Include s         ->
+	    path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p))
+	 | T.Include s                  ->
 	    begin 
-	       try Some (T.Include (List.assoc s st.requires))
-	       with Not_found -> None
+	       try path, Some (T.Include (List.assoc s st.requires))
+	       with Not_found -> path, None
 	    end
-	 | T.Coercion (b, 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
+	    if str <> "" then path, Some (T.Coercion (b, str)) else
+	    let base_uri = 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 (b, Filename.concat base_uri s))
-	 | item                -> Some item
+	    path, Some (T.Coercion (b, Filename.concat base_uri s))
+	 | T.Section (b, id, _) as item ->
+	    let path = if b then id :: path else List.tl path in
+	    path, Some item
+	 | item                         -> path, 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
@@ -190,8 +201,9 @@ let produce st =
       let lexbuf = Lexing.from_channel ich in
       try 
          let items = V8Parser.items V8Lexer.token lexbuf in
-         close_in ich;
-         let items = List.rev (X.list_rev_map_filter filter items) in
+         close_in ich; 
+	 let _, rev_items = X.list_rev_map_filter_fold filter [] items in
+	 let items = List.rev rev_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 
@@ -201,6 +213,6 @@ let produce st =
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich 
    in
-   init st.input_package; 
+   init st.input_package; require st st.input_package "preamble"; 
    List.iter (produce st) st.files; 
    commit st st.input_package