all initialization code is now in the new matitaInit.ml module.

[helm.git] / helm / matita / matitaInit.ml

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
new file mode 100644 (file)
index 0000000..aab8156
--- /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)
+