-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 \
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
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
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
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 \
matitaExcPp.cmo \
matitaMisc.cmo \
matitaDb.cmo \
+ matitamakeLib.cmo \
+ matitaInit.cmo \
matitaSync.cmo \
matitaDisambiguator.cmo \
matitacleanLib.cmo \
matitacLib.cmo \
$(NULL)
CLEANCMOS = $(CCMOS)
-MAKECMOS = $(CCMOS) matitamakeLib.cmo
+MAKECMOS = $(CCMOS)
all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean matitamake
mysql \
helm-registry \
helm-cic_disambiguation \
+helm-paramodulation \
"
FINDLIB_CLEANREQUIRES="$FINDLIB_DEPREQUIRES"
FINDLIB_CREQUIRES="\
unix \
helm-cic_omdoc \
helm-tactics \
-helm-paramodulation \
helm-xml \
"
FINDLIB_REQUIRES="\
(** {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} *)
(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"
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
--- /dev/null
+(* 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)
+
--- /dev/null
+(* 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
+
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
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
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
module MK = MatitamakeLib ;;
let _ =
- Helm_registry.load_from BuildTimeConf.matita_conf;
+ MatitaInit.load_config_only ();
MK.initialize ()
;;
* http://helm.cs.unibo.it/
*)
-(* ALB to link paramodulation... *)
-let _ = Paramodulation.Saturation.init ()
-
-
let _ =
let _ = Topdirs.dir_quit in
Toploop.loop Format.std_formatter;
projects / helm.git / commitdiff