]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
Procedural: we corrected two errors about the handling of mutcase (the "cases"
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index 4504d2999e9f7b51646152dc316a1ac86c2cc6b6..027b03575589bbd6ce3a1a747698b854798ddf3f 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 = [];
@@ -236,15 +234,22 @@ 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_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;