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

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index e793a725b61b3019c81ca31242729ce5c1d5d4f8..aff7895172e705f82c68fe3d71ee38bff21e185a 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -63,26 +63,6 @@ let dump f =
    Helm_registry.set_bool "matita.moo" false;
    let floc = H.dummy_floc in
    let nl_ast = G.Comment (floc, G.Note (floc, "")) in
-   let och = open_out f in
-   let out_comment och s =
-      let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
-      Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
-   in
-   let out_line_comment och s =
-      let l = 70 - String.length s in
-      let s = Printf.sprintf " %s %s" s (String.make l '*') in
-      out_comment och s
-   in
-   let out_preamble och (path, lines) =
-      let ich = open_in path in
-      let rec print i =
-         if i > 0 then 
-            let s = input_line ich in
-            begin Printf.fprintf och "%s\n" s; print (pred i) end
-      in 
-      print lines;
-      out_line_comment och "This file was automatically generated: do not edit"
-   in
    let pp_ast_statement st =
      GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
        ~map_unicode_to_tex:(Helm_registry.get_bool
@@ -90,11 +70,9 @@ let dump f =
        ~lazy_term_pp:CicNotationPp.pp_term 
        ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
    in
+   let och = open_out f in
    let nl () =  output_string och (pp_ast_statement nl_ast) in
-   let rt_base_dir = Filename.dirname Sys.argv.(0) in
-   let path = Filename.concat rt_base_dir "matita.ma.templ" in
-   let lines = 14 in
-   out_preamble och (path, lines);
+   MatitaMisc.out_preamble och;
    let grafite_parser_cb fname = 
       let ast = G.Executable 
         (floc, G.Command (floc, G.Include (floc, fname))) in