X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMisc.ml;h=687cb94f052de7c1068d90ec4a88ce62c91f7a1e;hb=2041f4fefe300f77338f6aea598f025f84db1bbc;hp=bb745f7030f968817f544fa4a49d1828eba4795e;hpb=863eeec8251791046ea6ea487286eb1434520725;p=helm.git

diff --git a/helm/software/matita/matitaMisc.ml b/helm/software/matita/matitaMisc.ml
index bb745f703..687cb94f0 100644
--- a/helm/software/matita/matitaMisc.ml
+++ b/helm/software/matita/matitaMisc.ml
@@ -155,7 +155,32 @@ let list_tl_at ?(equality=(==)) e l =
   aux l
 
 let shutup () = 
-  HLog.set_log_callback (fun _ _ -> ());
+  HLog.set_log_callback (fun _ _ -> ())
+(*
   let out = open_out "/dev/null" in
   Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
+*)
               
+(* FG: out_preamble *********************************************************)
+
+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 "*)" 
+ 
+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
+
+let out_preamble och =
+   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
+   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"