release snapshot

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 34b64284f85f3f0f99f7bbb13ae0b4cf5da1ddad..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,10 +42,34 @@ let wants s l =
 let already_configured s l =
   List.for_all (fun item -> List.exists (fun x -> x = item) l) s
   
+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
@@ -85,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
@@ -136,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
@@ -160,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",
@@ -190,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;
@@ -207,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 
@@ -222,3 +237,6 @@ let load_configuration_file () =
 let parse_cmdline () =
   status := parse_cmdline !status
 
+let fill_registry () =
+  status := fill_registry !status
+