]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
- transcript: bugfix
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index 4504d2999e9f7b51646152dc316a1ac86c2cc6b6..091987b65564602403396176e0fb28eb2278af42 100644 (file)
@@ -49,6 +49,7 @@ type status = {
    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;
@@ -115,13 +116,9 @@ let make registry =
    in
    load_registry registry;
    let input_type, input_ext = get_input_type "package.input_type" in 
-   let heading_lines = match input_type with
-      | T.Grafite -> 0
-      | _         -> R.get_int "transcript.heading_lines"
-   in
    let st = {
       heading_path = R.get_string "transcript.heading_path";
-      heading_lines = heading_lines;
+      heading_lines = R.get_int "transcript.heading_lines";
       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";
@@ -131,6 +128,7 @@ let make registry =
       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 = [];
@@ -242,9 +240,13 @@ let produce st =
         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_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 = get_items lexbuf in close_in ich;