From 51d82e0a8a4d4ed86d2646edb2654e565ac34a82 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 20 Sep 2005 10:51:26 +0000 Subject: [PATCH] all initialization code is now in the new matitaInit.ml module. --- helm/matita/.depend | 66 +++++++++++--------- helm/matita/Makefile.in | 7 ++- helm/matita/configure.ac | 2 +- helm/matita/matita.ml | 12 +--- helm/matita/matita.txt | 4 +- helm/matita/matitaInit.ml | 121 +++++++++++++++++++++++++++++++++++++ helm/matita/matitaInit.mli | 29 +++++++++ helm/matita/matitacLib.ml | 9 +-- helm/matita/matitaclean.ml | 7 +-- helm/matita/matitadep.ml | 3 +- helm/matita/matitamake.ml | 2 +- helm/matita/matitatop.ml | 4 -- 12 files changed, 199 insertions(+), 67 deletions(-) create mode 100644 helm/matita/matitaInit.ml create mode 100644 helm/matita/matitaInit.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index b4a1a4c35..d8a04bf10 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,23 +1,11 @@ -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - matitacleanLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - buildTimeConf.cmo -matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - buildTimeConf.cmx -matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \ - buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \ - buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaInit.cmi matitaGui.cmi \ + matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaInit.cmx matitaGui.cmx \ + matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi -matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo -matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ @@ -40,14 +28,12 @@ matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitacLib.cmx \ matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaMathView.cmx \ matitaLog.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \ matitaDisambiguator.cmx buildTimeConf.cmx matitaGui.cmi +matitaInit.cmo: matitamakeLib.cmi matitaDb.cmi buildTimeConf.cmo \ + matitaInit.cmi +matitaInit.cmx: matitamakeLib.cmx matitaDb.cmx buildTimeConf.cmx \ + matitaInit.cmi matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi -matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ - matitamakeLib.cmi -matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ - matitamakeLib.cmi -matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo -matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ buildTimeConf.cmo matitaMathView.cmi @@ -58,12 +44,6 @@ matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \ buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \ buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo -matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \ matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi @@ -76,6 +56,32 @@ matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx +matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + matitaDb.cmi buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + matitaDb.cmx buildTimeConf.cmx matitacLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + buildTimeConf.cmo +matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + buildTimeConf.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \ + buildTimeConf.cmo +matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \ + buildTimeConf.cmx +matitamake.cmo: matitamakeLib.cmi matitaInit.cmi +matitamake.cmx: matitamakeLib.cmx matitaInit.cmx +matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ + matitamakeLib.cmi +matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ + matitamakeLib.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 58b4fc60b..a519950b0 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -29,12 +29,13 @@ CMOS = \ matitaExcPp.cmo \ matitaMisc.cmo \ matitaDb.cmo \ + matitamakeLib.cmo \ + matitaInit.cmo \ matitaSync.cmo \ matitacleanLib.cmo \ matitaDisambiguator.cmo \ matitaEngine.cmo \ matitacLib.cmo \ - matitamakeLib.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ matitaGtkMisc.cmo \ @@ -49,6 +50,8 @@ CCMOS = \ matitaExcPp.cmo \ matitaMisc.cmo \ matitaDb.cmo \ + matitamakeLib.cmo \ + matitaInit.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ matitacleanLib.cmo \ @@ -56,7 +59,7 @@ CCMOS = \ matitacLib.cmo \ $(NULL) CLEANCMOS = $(CCMOS) -MAKECMOS = $(CCMOS) matitamakeLib.cmo +MAKECMOS = $(CCMOS) all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean matitamake diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 22ee37491..91ae69482 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -31,6 +31,7 @@ pcre \ mysql \ helm-registry \ helm-cic_disambiguation \ +helm-paramodulation \ " FINDLIB_CLEANREQUIRES="$FINDLIB_DEPREQUIRES" FINDLIB_CREQUIRES="\ @@ -38,7 +39,6 @@ $FINDLIB_CLEANREQUIRES \ unix \ helm-cic_omdoc \ helm-tactics \ -helm-paramodulation \ helm-xml \ " FINDLIB_REQUIRES="\ diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index bc06a56e5..45ad19556 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -31,17 +31,7 @@ open MatitaMisc (** {2 Initialization} *) -let _ = - Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation.load_notation BuildTimeConf.core_notation_script; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.create_owner_environment (); - MatitamakeLib.initialize (); - CicEnvironment.set_trust (* environment trust *) - (let trust = Helm_registry.get_bool "matita.environment_trust" in - fun _ -> trust); - Paramodulation.Saturation.init () +let _ = MatitaInit.initialize_all () (** {2 GUI callbacks} *) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 13d946afc..3ec54f51e 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -100,8 +100,6 @@ TODO (e.g. guardare output di matitac) - matitaclean (e famiglia) non cancellano le directory vuote (e per giunta il cicbrowser le mostra :-) - - codice di inizializzazione di matita, matitac, matitatop replicato e non - in sync - fattorizzare codice fra MatitaEngine e DisambiguatePp (dove, fra l'altro, ora io (=CSC) ho messo anche un parser!!!) - bug "Warn: baseuri cic:/matita/higher_order_defs/ordering is not empty" @@ -117,6 +115,8 @@ TODO DEMONI E ALTRO DONE +- codice di inizializzazione di matita, matitac, matitatop replicato e non + in sync -> Gares - tutte gli script che parsano (e.g. matitaclean, matitadep) debbono processare la notazione per evitare errori di parsing (visibili ora che e' stata committata la contrib list)! -> Gares diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml new file mode 100644 index 000000000..aab815601 --- /dev/null +++ b/helm/matita/matitaInit.ml @@ -0,0 +1,121 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +type thingsToInitilaize = + ConfigurationFile | Db | Environment | Getter | Notation | + Paramodulation | Makelib + +exception FailedToInitialize of thingsToInitilaize + +let wants s l = + List.iter ( + fun item -> + if not (List.exists (fun x -> x = item) l) then + raise (FailedToInitialize item)) + s + +let already_configured s l = + List.for_all (fun item -> List.exists (fun x -> x = item) l) s + +let load_configuration init_status = + if not (already_configured [ConfigurationFile] init_status) then + begin + Helm_registry.load_from BuildTimeConf.matita_conf; + ConfigurationFile::init_status + end + else + init_status + +let initialize_db init_status = + wants [ConfigurationFile] init_status; + if not (already_configured [Db] init_status) then + begin + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.create_owner_environment (); + Db::init_status + end + else + init_status + +let initialize_paramodulation init_status = + wants [] init_status; + if not (already_configured [Paramodulation] init_status) then + begin + Paramodulation.Saturation.init (); + Paramodulation::init_status + end + else + init_status + +let initialize_makelib init_status = + wants [ConfigurationFile] init_status; + if not (already_configured [Makelib] init_status) then + begin + MatitamakeLib.initialize (); + Makelib::init_status + end + else + init_status + +let initialize_notation init_status = + wants [ConfigurationFile] init_status; + if not (already_configured [Notation] init_status) then + begin + CicNotation.load_notation BuildTimeConf.core_notation_script; + Notation::init_status + end + else + init_status + +let initialize_environment init_status = + wants [ConfigurationFile] init_status; + if not (already_configured [Getter;Environment] init_status) then + begin + Http_getter.init (); + CicEnvironment.set_trust (* environment trust *) + (let trust = Helm_registry.get_bool "matita.environment_trust" in + fun _ -> trust); + Getter::Environment::init_status + end + else + init_status + +let status = ref [] + +let initialize_all () = + status := + initialize_notation + (initialize_environment + (initialize_db + (initialize_paramodulation + (initialize_makelib + (load_configuration !status))))) + +let load_config_only () = + status := load_configuration !status + +let initialize_notation () = + status := initialize_notation (load_configuration !status) + diff --git a/helm/matita/matitaInit.mli b/helm/matita/matitaInit.mli new file mode 100644 index 000000000..be6abfc7a --- /dev/null +++ b/helm/matita/matitaInit.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val load_config_only: unit -> unit +val initialize_all: unit -> unit +val initialize_notation: unit -> unit + diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index a795f5f4b..209919980 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -167,14 +167,7 @@ let dump_moo_to_file file moo = close_out os let main ~mode = - Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation.load_notation BuildTimeConf.core_notation_script; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.create_owner_environment (); - CicEnvironment.set_trust (* environment trust *) - (let trust = Helm_registry.get_bool "matita.environment_trust" in - fun _ -> trust); + MatitaInit.initialize_all (); status := Some (ref (Lazy.force MatitaEngine.initial_status)); Sys.catch_break true; let origcb = MatitaLog.get_log_callback () in diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index f42973f90..1a11f5fa1 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -26,12 +26,7 @@ module UM = UriManager;; module TA = GrafiteAst;; -let _ = - Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation.load_notation BuildTimeConf.core_notation_script; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.create_owner_environment () +let _ = MatitaInit.initialize_all () let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 4e260dcf6..70240068f 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -96,8 +96,7 @@ let process_notation_of_file file = raise exn let main () = - Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation.load_notation BuildTimeConf.core_notation_script; + MatitaInit.initialize_notation (); let files = ref [] in Arg.parse arg_spec (add_l files) usage; List.iter diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml index e9efc3822..5a3ecf5ee 100644 --- a/helm/matita/matitamake.ml +++ b/helm/matita/matitamake.ml @@ -26,7 +26,7 @@ module MK = MatitamakeLib ;; let _ = - Helm_registry.load_from BuildTimeConf.matita_conf; + MatitaInit.load_config_only (); MK.initialize () ;; diff --git a/helm/matita/matitatop.ml b/helm/matita/matitatop.ml index fe7d41c88..bdf9860b1 100644 --- a/helm/matita/matitatop.ml +++ b/helm/matita/matitatop.ml @@ -23,10 +23,6 @@ * http://helm.cs.unibo.it/ *) -(* ALB to link paramodulation... *) -let _ = Paramodulation.Saturation.init () - - let _ = let _ = Topdirs.dir_quit in Toploop.loop Format.std_formatter; -- 2.39.2