MaTeX

[helm.git] / matita / components / binaries / matex / engine.ml

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 5a1a3e3454a6b05e3a4f59878056f3d5afeeb8aa..165986b473e9a115fc0d6068ae4255f6e00889e5 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -141,8 +141,8 @@ let rec proc_proof st ris c t = match t with
       let is_w = proc_term [] c w in
       let ris = mk_open st ris in
       proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
-   | C.Appl ts              ->
-      let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
+   | C.Appl (t0 :: ts)     ->
+      let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in
       let ris = T.Macro "STEP" :: mk_inferred st c t ris in
       let tts = L.rev_map (proc_term [] c) rts in
       mk_exit st (T.rev_mk_args tts ris)
@@ -174,17 +174,24 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with
 
 (* top level processing *)
 
+let note = T.Note "This file was automatically generated by MaTeX: do not edit"
+
 let proc_item item s t =
    let is = [T.Macro "end"; T.arg item] in
-   T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
+   note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
 
 let proc_top_proof s t =
    let tt = A.process_top_term s t in (* anticipation *)
-   let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"] in
+   let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
 
 let open_out_tex s =
-   open_out (F.concat !G.out_dir (s ^ T.file_ext))
+   let fname = s ^ T.file_ext in
+   begin match !G.list_och with
+      | None     -> ()
+      | Some och -> P.fprintf och "%s\n" fname
+   end;
+   open_out (F.concat !G.out_dir fname)
 
 let proc_pair s ss u = function
    | None   ->