X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;h=fec223b006c2f7fc99b8cda7adb4b4f0689ae53f;hb=9ffc433e8913660620b1dd4ce4c22db1e42c7562;hp=84dff49e9eced28ba3de448426503fc6550f0d56;hpb=6d1af82b714e5c6a7f33534d6832598e72cb23c3;p=helm.git

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 84dff49e9..fec223b00 100644
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -23,11 +23,12 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 type thingsToInitilaize = 
-  ConfigurationFile | Db | Environment | Getter | Notation | 
-  Paramodulation | Makelib | CmdLine
+  ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -41,10 +42,21 @@ let wants s l =
 let already_configured s l =
   List.for_all (fun item -> List.exists (fun x -> x = item) l) s
   
+let tilde_expand_key k =
+  try
+    Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
+  with Helm_registry.Key_not_found _ -> ()
+
 let load_configuration init_status =
   if not (already_configured [ConfigurationFile] init_status) then
     begin
       Helm_registry.load_from BuildTimeConf.matita_conf;
+      if not (Helm_registry.has "user.name") then begin
+        let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
+        Helm_registry.set "user.name" login
+      end;
+      tilde_expand_key "matita.basedir";
+      tilde_expand_key "user.home";
       ConfigurationFile::init_status 
     end
   else
@@ -55,22 +67,12 @@ 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
     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
@@ -81,16 +83,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
@@ -149,10 +141,13 @@ let usage () =
   try Hashtbl.find usages usage_key with Not_found -> default_usage
 
 let registry_defaults =
-  [ "matita.debug", "false";
-    "matita.quiet", "false";
-    "matita.preserve", "false";
-    "db.nodb", "false";
+  [
+    "db.nodb",                  "false";
+    "matita.debug",             "false";
+    "matita.external_editor",   "gvim -f -c 'go %p' %f";
+    "matita.preserve",          "false";
+    "matita.quiet",             "false";
+    "matita.profile",           "true";
   ]
 
 let set_registry_values =
@@ -160,7 +155,7 @@ let set_registry_values =
 
 let parse_cmdline init_status =
   if not (already_configured [CmdLine] init_status) then begin
-    let includes = ref [] in
+    let includes = ref [ BuildTimeConf.stdlib_dir ] in
     let args = ref [] in
     let add_l l = fun s -> l := s :: !l in
     let arg_spec =
@@ -176,6 +171,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
@@ -195,6 +193,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
@@ -205,20 +205,19 @@ let die_usage () =
 
 let initialize_all () =
   status := 
-    initialize_notation 
+    List.fold_left (fun s f -> f s) !status
+      [ parse_cmdline; load_configuration; initialize_makelib;
+        initialize_db; initialize_environment ]
+(*     initialize_notation 
       (initialize_environment 
         (initialize_db 
-          (initialize_paramodulation 
-            (initialize_makelib
-              (load_configuration
-                (parse_cmdline !status))))))
+          (initialize_makelib
+            (load_configuration
+              (parse_cmdline !status))))) *)
 
 let load_configuration_file () =
   status := load_configuration !status
 
-let initialize_notation () =
-  status := initialize_notation (load_configuration !status)
-
 let parse_cmdline () =
   status := parse_cmdline !status