From 5965234ea82419215b121405fc6dfc53abe4b491 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 Jul 2005 14:49:51 +0000 Subject: [PATCH] function to domp moo_content is now exported --- helm/matita/matitacLib.ml | 21 ++++++++++++++++----- helm/matita/matitacLib.mli | 1 + 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index d4bd0aafe..ba2085bca 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -115,6 +115,21 @@ let go () = Sys.catch_break true; interactive_loop () +let clean_exit n = + match !status with + None -> exit n + | Some status -> + let baseuri = MatitaTypes.get_string_option !status "baseuri" in + MatitacleanLib.clean_baseuris ~verbose:false [baseuri]; + exit n + +let dump_moo_to_file file moo = + let os = open_out (MatitaMisc.obj_file_of_script file) in + let output s = output_string os s in + output "(* GENERATED FILE: DO NOT EDIT! *)\n\n"; + List.iter output (List.rev moo); + close_out os + let main ~mode = Helm_registry.load_from "matita.conf.xml"; Http_getter.init (); @@ -156,11 +171,7 @@ let main ~mode = end else begin - let os = open_out (MatitaMisc.obj_file_of_script fname) in - let output s = output_string os s in - output "(* GENERATED FILE: DO NOT EDIT! *)\n\n"; - List.iter output (List.rev moo_content_rev); - close_out os; + dump_moo_to_file fname moo_content_rev; MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); exit 0 diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli index 8032320ce..a053a3f1a 100644 --- a/helm/matita/matitacLib.mli +++ b/helm/matita/matitacLib.mli @@ -28,6 +28,7 @@ val interactive_loop : unit -> unit (** go initializes the status and calls interactive_loop *) val go : unit -> unit val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit +val dump_moo_to_file: string -> string list -> unit (** clean_exit n performs an exit [n] after a complete clean-up of what was partially compiled -- 2.39.2