- MatitaMisc: we factorized here the function out_preamble used in matitadep

[helm.git] / helm / software / components / binaries / transcript / engine.ml

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 027b03575589bbd6ce3a1a747698b854798ddf3f..2e81186ea7e91c75e7a51016ea94b20a8ca20eba 100644 (file)
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -50,6 +50,7 @@ type status = {
    output_type: T.output_kind;
    input_ext: string;
    remove_lines: int;
+   excludes: string list;
    includes: (string * string) list;
    coercions: (string * string) list;
    files: string list;
@@ -75,12 +76,13 @@ 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_ext 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
-         | None   -> List.rev files
-        | Some l -> aux (trim l :: files)
+   let rec aux files = match eof ich with
+      | None   -> List.rev files
+      | Some l ->
+        let l = trim l in
+        if List.mem l st.excludes then aux files else aux (l :: files)
    in 
    let files = aux [] in
    let _ = Unix.close_process_in ich in
@@ -116,6 +118,10 @@ let make registry =
    in
    load_registry registry;
    let input_type, input_ext = get_input_type "package.input_type" in 
+   let excludes = match input_type with
+      | T.Grafite  -> ["theory"]
+      | T.Gallina8 -> []
+   in
    let st = {
       heading_path = R.get_string "transcript.heading_path";
       heading_lines = R.get_int "transcript.heading_lines";
@@ -129,6 +135,7 @@ let make registry =
       output_type = get_output_type "package.output_type";
       input_ext = input_ext;
       remove_lines = R.get_int "package.heading_lines";
+      excludes = excludes;
       includes = get_pairs "package.include";
       coercions = get_pairs "package.coercion";
       files = [];