X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;fp=helm%2Fmatita%2FmatitaInit.ml;h=d0127530870c0e53295f25eb67e0a2c88d736056;hb=56187138970c77cf6b219224c0dc510fa786e7cd;hp=1e9ebe2dd2b2eb539ea7096816fd3a131ba1578b;hpb=c72b0d76d607482bccf12e7193a4d1a777815b91;p=helm.git

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 1e9ebe2dd..d01275308 100644
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -155,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 =
@@ -178,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
@@ -197,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