+module HR = Helm_registry
+
+let print_times msg =
+ let times = Unix.times () in
+ let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in
+ Printf.printf "TIME STAMP: %s: %f\n" msg stamp; flush stdout; stamp
+
+let fix_name f =
+ let f =
+ if Pcre.pmatch ~pat:"^\\./" f then String.sub f 2 (String.length f - 2)
+ else f
+ in
+ HExtlib.normalize_path f
+
+(* FG: old function left for reference *)
+let exclude excluded_files files =
+ let map file = not (List.mem (fix_name file) excluded_files) in
+ List.filter map files
+
+let generate_theory theory_file deps =
+ if theory_file = "" then deps else
+ let map (files, deps) (t, d) =
+ if t = theory_file then files, deps else
+ S.add t files, List.fold_left (fun deps dep -> S.add dep deps) deps d
+ in
+ let out_include och dep =
+ Printf.fprintf och "include \"%s\".\n\n" dep
+ in
+ let fileset, depset = List.fold_left map (S.empty, S.empty) deps in
+ let top_depset = S.diff fileset depset in
+ let och = open_out theory_file in
+ begin
+ MatitaMisc.out_preamble och;
+ S.iter (out_include och) top_depset;
+ close_out och;
+ (theory_file, S.elements top_depset) :: deps
+ end
+