release work snapshot ...

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index fec223b006c2f7fc99b8cda7adb4b4f0689ae53f..8223416e4dd7d632846e7963927bef57e700948e 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -56,6 +56,10 @@ let load_configuration init_status =
         Helm_registry.set "user.name" login
       end;
       tilde_expand_key "matita.basedir";
+      if Helm_registry.get_bool "matita.system" then begin
+        prerr_endline "SISTEMA";
+        Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir;
+      end;
       tilde_expand_key "user.home";
       ConfigurationFile::init_status 
     end
@@ -66,7 +70,8 @@ let initialize_db init_status =
   wants [ ConfigurationFile; CmdLine ] init_status;
   if not (already_configured [ Db ] init_status) then
     begin
-      MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+      if not (Helm_registry.get_bool "matita.system") then
+        MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
       LibraryDb.create_owner_environment ();
       Db::init_status
     end
@@ -143,6 +148,7 @@ let usage () =
 let registry_defaults =
   [
     "db.nodb",                  "false";
+    "matita.system",            "false";
     "matita.debug",             "false";
     "matita.external_editor",   "gvim -f -c 'go %p' %f";
     "matita.preserve",          "false";
@@ -169,8 +175,12 @@ let parse_cmdline init_status =
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
           "Turns off automatic baseuri cleaning";
         "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
-              ("Avoid using external database connection "
-               ^ "(WARNING: disable many features)");
+            ("Avoid using external database connection "
+             ^ "(WARNING: disable many features)");
+        "-system", Arg.Unit (fun () ->
+              Helm_registry.set_bool "matita.system" true),
+            ("Act on the system library instead of the user one"
+             ^ "(WARNING: not for the casual user)");
         "-noprofile", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
           "Turns off profiling printings";