X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;h=d0127530870c0e53295f25eb67e0a2c88d736056;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9ea9e07d2670d89729b3b9fe5eafbbc9487a928f;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index 9ea9e07d2..d01275308 100644 --- 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 @@ -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