added default for matita.noiinertypes

[helm.git] / matita / matitaInit.ml

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index 88f5c9c35325356f51c7315fd7ad2e8ed53243dd..3beb85ca61c10f3092e1be2195d004918c73a106 100644 (file)
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -50,7 +50,8 @@ let registry_defaults = [
   "matita.system",               "false";
   "matita.verbosity",            "1";
   "matita.bench",                "false";
-  "matita.paste_unicode_as_tex", "false"
+  "matita.paste_unicode_as_tex", "false";
+  "matita.noinnertypes",         "false";
     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
      * intuitively verbose *)
 ]
@@ -59,7 +60,6 @@ let set_registry_values =
   List.iter (fun key, value -> Helm_registry.set ~key ~value)
 
 let fill_registry init_status =
-  wants [ ConfigurationFile ] init_status;
   if not (already_configured [ Registry ] init_status) then begin
     set_registry_values registry_defaults;
     Registry :: init_status
@@ -113,7 +113,7 @@ let initialize_makelib init_status =
     init_status
 
 let initialize_environment init_status = 
-  wants [ConfigurationFile] init_status;
+  wants [CmdLine] init_status;
   if not (already_configured [Getter;Environment] init_status) then
     begin
       Http_getter.init ();
@@ -225,6 +225,7 @@ let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 
 let parse_cmdline init_status =
   if not (already_configured [CmdLine] init_status) then begin
+    wants [Registry] init_status;
     let includes = ref [] in
     let default_includes = [ 
       ".";
@@ -239,9 +240,13 @@ let parse_cmdline init_status =
     let reduce_verbosity () =
       Helm_registry.set_int "matita.verbosity"
         (Helm_registry.get_int "matita.verbosity" - 1) in
+    let print_version () =
+            Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
     let increase_verbosity () =
       Helm_registry.set_int "matita.verbosity"
         (Helm_registry.get_int "matita.verbosity" + 1) in
+    let no_innertypes () =
+      Helm_registry.set_bool "matita.noinnertypes" false in
     let arg_spec =
       let std_arg_spec = [
         "-I", Arg.String (add_l includes),
@@ -257,6 +262,8 @@ let parse_cmdline init_status =
         "-noprofile", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
           "Turns off profiling printings";
+        "-noinnertypes", Arg.Unit no_innertypes, 
+          "Turns off inner types generation while publishing";
         "-profile-only",
           Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
           "Activates only profiler with label matching the provided regex";
@@ -272,6 +279,7 @@ let parse_cmdline init_status =
             ("Act on the system library instead of the user one"
              ^ "\n    WARNING: not for the casual user");
         "-v", Arg.Unit increase_verbosity, "Increase verbosity";
+        "--version", Arg.Unit print_version, "Prints version";
       ] in
       let debug_arg_spec =
         if BuildTimeConf.debug then
@@ -312,7 +320,7 @@ let die_usage () =
   exit 1
 
 let conf_components = 
-  [ parse_cmdline; load_configuration; fill_registry ]
+  [ load_configuration; fill_registry; parse_cmdline]
 
 let other_components =
   [ initialize_makelib; initialize_db; initialize_environment ]
@@ -331,6 +339,8 @@ let initialize_all () =
 let parse_cmdline_and_configuration_file () =
   status := List.fold_left (fun s f -> f s) !status conf_components
 
-;;
+let initialize_environment () =
+  status := initialize_environment !status
 
-Inversion_principle.init ()
+let _ =
+  Inversion_principle.init ()