X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=027b03575589bbd6ce3a1a747698b854798ddf3f;hb=4446f96e1829f1a82fc71cb49d8ddc392e73b155;hp=ccf07423f6dd5cc14b5af35f6ede71356a5bbc2f;hpb=0b76904a3f10bfd6390d26172fd6979626bd72f4;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index ccf07423f..027b03575 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -46,8 +46,10 @@ type status = {
    output_base_uri: string;
    input_path: string;
    output_path: string;
-   input_type: string;
+   input_type: T.input_kind;
    output_type: T.output_kind;
+   input_ext: string;
+   remove_lines: int;
    includes: (string * string) list;
    coercions: (string * string) list;
    files: string list;
@@ -72,8 +74,8 @@ let load_registry registry =
 
 let set_files st =
    let eof ich = try Some (input_line ich) with End_of_file -> None in
-   let trim l = Filename.chop_extension (Str.string_after l 2) in
-   let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.input_type in
+   let trim l = Filename.chop_extension (Str.string_after l 2) in 
+   let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.input_ext in
    let ich = Unix.open_process_in cmd in
    let rec aux files =
       match eof ich with
@@ -100,6 +102,12 @@ let init () =
 let make registry =
    let id x = x in
    let get_pairs = R.get_list (R.pair id id) in 
+   let get_input_type key =
+      match R.get_string key with
+         | "gallina8" -> T.Gallina8, ".v"
+	 | "grafite"  -> T.Grafite, ".ma"
+	 | _          -> failwith "unknown input type"
+   in
    let get_output_type key =
       match R.get_string key with
          | "procedural"  -> T.Procedural
@@ -107,6 +115,7 @@ let make registry =
 	 | _             -> failwith "unknown output type"
    in
    load_registry registry;
+   let input_type, input_ext = get_input_type "package.input_type" in 
    let st = {
       heading_path = R.get_string "transcript.heading_path";
       heading_lines = R.get_int "transcript.heading_lines";
@@ -116,8 +125,10 @@ let make registry =
       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";
-      input_type = R.get_string "package.input_type";
+      input_type = input_type;
       output_type = get_output_type "package.output_type";
+      input_ext = input_ext;
+      remove_lines = R.get_int "package.heading_lines";
       includes = get_pairs "package.include";
       coercions = get_pairs "package.coercion";
       files = [];
@@ -126,7 +137,8 @@ let make registry =
    } in
    let st = {st with
       heading_path = Filename.concat !O.cwd st.heading_path;
-      output_path = Filename.concat !O.cwd st.output_path;
+      input_path = Filename.concat !O.cwd st.input_path;
+      output_path = Filename.concat !O.cwd st.output_path
    } in
    prerr_endline "reading file names ...";
    let st = set_files st in
@@ -154,7 +166,7 @@ let set_items st name items =
    let contents = List.rev_append items script.contents in
    st.scripts.(i) <- {script with name = name; contents = contents}
    
-let set_heading st name =
+let set_heading st name = 
    let heading = st.heading_path, st.heading_lines in
    set_items st name [T.Heading heading] 
    
@@ -193,6 +205,10 @@ let produce st =
       | T.Notation (false, _) -> false
       | _                     -> true
    in
+   let get_items = match st.input_type with
+      | T.Gallina8 -> Gallina8Parser.items Gallina8Lexer.token
+      | T.Grafite  -> GrafiteParser.items GrafiteLexer.token
+   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
@@ -218,19 +234,25 @@ let produce st =
 	 | T.Section (b, id, _) as item ->
 	    let path = if b then id :: path else List.tl path in
 	    path, Some item
+	 | T.Verbatim s                 ->
+	    let pat, templ = st.input_base_uri, st.output_base_uri in
+	    path, Some (T.Verbatim (Pcre.replace ~pat ~templ s)) 
 	 | item                         -> path, Some item
       in
       let set_includes st name =
       	 try require st name (List.assoc name st.includes) 
 	 with Not_found -> ()
       in
+      let rec remove_lines ich n =
+         if n > 0 then let _ =  input_line ich in remove_lines ich (pred n)
+      in
       Printf.eprintf "processing file name: %s ...\n" name; flush stderr; 
-      let file = Filename.concat st.input_path (name ^ st.input_type) in
+      let file = Filename.concat st.input_path (name ^ st.input_ext) in
       let ich = open_in file in
+      begin try remove_lines ich st.remove_lines with End_of_file -> () end;
       let lexbuf = Lexing.from_channel ich in
       try 
-         let items = V8Parser.items V8Lexer.token lexbuf in
-         close_in ich; 
+         let items = get_items lexbuf 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