let conffile = ref BuildTimeConf.matita_conf
let registry_defaults = [
- "db.nodb", "false";
- "matita.debug", "false";
- "matita.external_editor", "gvim -f -c 'go %p' %f";
- "matita.preserve", "false";
- "matita.profile", "true";
- "matita.system", "false";
- "matita.verbosity", "1";
- "matita.bench", "false";
+ "matita.debug", "false";
+ "matita.external_editor", "gvim -f -c 'go %p' %f";
+ "matita.preserve", "false";
+ "matita.profile", "true";
+ "matita.system", "false";
+ "matita.verbosity", "1";
+ "matita.bench", "false";
+ "matita.paste_unicode_as_tex", "false"
(** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
* intuitively verbose *)
]
let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
Helm_registry.set "user.name" login
end;
+ let home = Helm_registry.get_string "matita.basedir" in
+ let user_conf_file = home ^ "/matita.conf.xml" in
+ if HExtlib.is_regular user_conf_file then
+ begin
+ HLog.message ("Loading additional conf file from " ^ user_conf_file);
+ try
+ Helm_registry.load_from user_conf_file
+ with exn ->
+ HLog.error
+ ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
+ end;
ConfigurationFile::init_status
end
else
"-force",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
("Force actions that would not be executed per default");
- "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
- ("Avoid using external database connection"
- ^ "\n WARNING: disable many features");
"-noprofile",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
"Turns off profiling printings";