X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=8009483f14028221e4786531f3b9affaf5debb1c;hb=fd4196b476bff30c46a80cd858ea7bf057f301eb;hp=7e561e9b0468412fa649ee0785aa58f019af00be;hpb=298868e07163c21863d542136733d24bfbec2482;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 7e561e9b0..8009483f1 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -29,7 +29,8 @@ module T = Types
 module G = Grafite
 
 type script = {
-   name: string;
+   name    : string;
+   is_ma   : bool;
    contents: T.items
 }
 
@@ -51,7 +52,7 @@ type status = {
 }
 
 let default_script = { 
-   name = ""; contents = []
+   name = ""; is_ma = false; contents = []
 }
 
 let default_scripts = 2
@@ -134,20 +135,21 @@ let get_index st name =
       | Some i, _ | _, Some i -> i
       | None, None            -> failwith "not enought script entries"
 
+let is_ma st name =
+   let i = get_index st name in
+   let script = st.scripts.(i) in
+   st.scripts.(i) <- {script with is_ma = true}
+
 let set_items st name items =
    let i = get_index st name in
    let script = st.scripts.(i) in
    let contents = List.rev_append items script.contents in
-   st.scripts.(i) <- {name = name; contents = contents}
+   st.scripts.(i) <- {script with name = name; contents = contents}
    
 let set_heading st name =
    let heading = st.heading_path, st.heading_lines in
    set_items st name [T.Heading heading] 
    
-let set_baseuri st name =
-   let baseuri = Filename.concat st.output_base_uri name in
-   set_items st name [T.BaseUri baseuri]
-   
 let require st name inc =
    set_items st name [T.Include inc]
 
@@ -160,20 +162,24 @@ let make_path path =
 let make_prefix path =
    String.concat "__" (List.rev path) ^ "__"
 
+let make_script_name st script name = 
+   let ext = if script.is_ma then ".ma" else ".mma" in
+   Filename.concat st.output_path (name ^ ext)
+
 let commit st name =
    let i = get_index st name in
    let script = st.scripts.(i) in
    let path = Filename.concat st.output_path (Filename.dirname name) in
-   let name = Filename.concat st.output_path (name ^ ".ma") in
+   let name = make_script_name st script name in
    let cmd = Printf.sprintf "mkdir -p %s" path in
    let _ = Sys.command cmd in
    let och = open_out name in
    G.commit st.output_type och script.contents;
    close_out och;
-   st.scripts.(i) <-  default_script
-   
+   st.scripts.(i) <- default_script
+
 let produce st =
-   let init name = set_heading st name; set_baseuri st name in
+   let init name = set_heading st name in
    let partition = function 
       | T.Coercion (false, _)
       | T.Notation (false, _) -> false
@@ -183,13 +189,13 @@ let produce st =
       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 path = function
-         | T.Inline (b, k, obj, p)      -> 
+         | T.Inline (b, k, obj, p, f)   -> 
 	    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
-	    path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p))
+	    path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p, f))
 	 | T.Include s                  ->
 	    begin 
 	       try path, Some (T.Include (List.assoc s st.requires))
@@ -224,6 +230,7 @@ let produce st =
       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"; 
    List.iter (produce st) st.files; 
    commit st st.input_package