Huge reorganization of matita and ocaml.

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 1e9ebe2dd2b2eb539ea7096816fd3a131ba1578b..c47bcb1649138f3ee47e8ccd6c4b9098e835cc43 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -26,7 +26,7 @@
 open Printf
 
 type thingsToInitilaize = 
-  ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
+  ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -65,7 +65,7 @@ let initialize_db init_status =
   if not (already_configured [ Db ] init_status) then
     begin
       MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
-      MatitaDb.create_owner_environment ();
+      LibraryDb.create_owner_environment ();
       Db::init_status
     end
   else
@@ -81,16 +81,6 @@ let initialize_makelib init_status =
   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
@@ -155,6 +145,7 @@ let registry_defaults =
     "matita.external_editor",   "gvim -f -c 'go %p' %f";
     "matita.preserve",          "false";
     "matita.quiet",             "false";
+    "matita.profile",           "true";
   ]
 
 let set_registry_values =
@@ -178,6 +169,9 @@ let parse_cmdline init_status =
         "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
               ("Avoid using external database connection "
                ^ "(WARNING: disable many features)");
+        "-noprofile", 
+          Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
+          "Turns off profiling printings";
       ] in
       let debug_arg_spec =
         if BuildTimeConf.debug then
@@ -197,6 +191,8 @@ let parse_cmdline init_status =
     Arg.parse arg_spec (add_l args) (usage ());
     set_list ~key:"matita.includes" includes;
     set_list ~key:"matita.args" args;
+    HExtlib.set_profiling_printings 
+      (fun () -> Helm_registry.get_bool "matita.profile");
     CmdLine :: init_status
   end else
     init_status
@@ -209,7 +205,7 @@ let initialize_all () =
   status := 
     List.fold_left (fun s f -> f s) !status
       [ parse_cmdline; load_configuration; initialize_makelib;
-        initialize_db; initialize_environment; initialize_notation ]
+        initialize_db; initialize_environment ]
 (*     initialize_notation 
       (initialize_environment 
         (initialize_db 
@@ -220,9 +216,6 @@ let initialize_all () =
 let load_configuration_file () =
   status := load_configuration !status
 
-let initialize_notation () =
-  status := initialize_notation (load_configuration !status)
-
 let parse_cmdline () =
   status := parse_cmdline !status