removed no longer used METAs

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 086932f6fab3ac8c5b4c5147561fc1374911abfc..53ff6b9d60f29bdb8d775ba61811f11b174e18ff 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -28,7 +28,7 @@
 open Printf
 
 type thingsToInitilaize = 
-  ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine
+  ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -42,21 +42,40 @@ 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 conffile = ref BuildTimeConf.matita_conf
+
+let registry_defaults =
+  [
+    "db.nodb",                  "false";
+    "matita.system",            "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 =
+  List.iter (fun key, value -> Helm_registry.set ~key ~value)
+
+let fill_registry init_status =
+  if not (already_configured [ Registry ] init_status) then begin
+    set_registry_values registry_defaults;
+    Registry :: init_status
+  end else
+    init_status
 
 let load_configuration init_status =
+  wants [ Registry ] init_status;
   if not (already_configured [ConfigurationFile] init_status) then
     begin
-      Helm_registry.load_from BuildTimeConf.matita_conf;
+      Helm_registry.load_from !conffile;
       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";
+      if Helm_registry.get_bool "matita.system" then
+        Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir;
       ConfigurationFile::init_status 
     end
   else
@@ -66,7 +85,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
@@ -89,7 +109,9 @@ let initialize_environment init_status =
     begin
       Http_getter.init ();
       CicEnvironment.set_trust (* environment trust *)
-        (let trust = Helm_registry.get_bool "matita.environment_trust" in
+        (let trust =
+          Helm_registry.get_opt_default Helm_registry.get_bool
+            ~default:true "matita.environment_trust" in
          fun _ -> trust);
       Getter::Environment::init_status
     end
@@ -140,22 +162,9 @@ let usage () =
   in
   try Hashtbl.find usages usage_key with Not_found -> default_usage
 
-let registry_defaults =
-  [
-    "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 =
-  List.iter (fun key, value -> Helm_registry.set ~key ~value)
-
 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 =
@@ -163,14 +172,21 @@ let parse_cmdline init_status =
         "-I", Arg.String (add_l includes),
           ("<path> Adds path to the list of searched paths for the "
            ^ "include command");
+        "-conffile", Arg.Set_string conffile,
+          (Printf.sprintf "<filename> Read configuration from filename (default: %s)" 
+            BuildTimeConf.matita_conf);
         "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true),
           "Turn off verbose compilation";
         "-preserve",
           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";
@@ -189,7 +205,6 @@ let parse_cmdline init_status =
     let set_list ~key l =
       Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)
     in
-    set_registry_values registry_defaults;
     Arg.parse arg_spec (add_l args) (usage ());
     set_list ~key:"matita.includes" includes;
     set_list ~key:"matita.args" args;
@@ -206,7 +221,8 @@ let die_usage () =
 let initialize_all () =
   status := 
     List.fold_left (fun s f -> f s) !status
-      [ parse_cmdline; load_configuration; initialize_makelib;
+    [ fill_registry;
+        parse_cmdline; load_configuration; initialize_makelib;
         initialize_db; initialize_environment ]
 (*     initialize_notation 
       (initialize_environment 
@@ -221,3 +237,6 @@ let load_configuration_file () =
 let parse_cmdline () =
   status := parse_cmdline !status
 
+let fill_registry () =
+  status := fill_registry !status
+