fixed cicbrowser.opt argv.(0)

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 9ea9e07d2670d89729b3b9fe5eafbbc9487a928f..44f6681833c40408e75dc3ec61f6ba46db95be86 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -40,10 +40,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
@@ -54,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
@@ -74,7 +85,7 @@ 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;
+      CicNotation2.load_notation BuildTimeConf.core_notation_script;
       Notation::init_status
     end
   else
@@ -144,6 +155,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 =
@@ -167,6 +179,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
@@ -186,6 +201,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