X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;h=53ff6b9d60f29bdb8d775ba61811f11b174e18ff;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=8223416e4dd7d632846e7963927bef57e700948e;hpb=67fea0e3bea686e59148d13765e20103f9373d24;p=helm.git

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 8223416e4..53ff6b9d6 100644
--- 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,25 +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";
-      if Helm_registry.get_bool "matita.system" then begin
-        prerr_endline "SISTEMA";
+      if Helm_registry.get_bool "matita.system" then
         Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir;
-      end;
-      tilde_expand_key "user.home";
       ConfigurationFile::init_status 
     end
   else
@@ -94,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
@@ -145,20 +162,6 @@ let usage () =
   in
   try Hashtbl.find usages usage_key with Not_found -> default_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";
-    "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 [ BuildTimeConf.stdlib_dir ] in
@@ -169,6 +172,9 @@ 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",
@@ -199,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;
@@ -216,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 
@@ -231,3 +237,6 @@ let load_configuration_file () =
 let parse_cmdline () =
   status := parse_cmdline !status
 
+let fill_registry () =
+  status := fill_registry !status
+