]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matitaInit.ml
better documentation both with -h and with F1
[helm.git] / matita / matitaInit.ml
index e9d447c1197c07503998e01b21b8612979c6fc13..03de96b5ff872982d78639edbc9b4453fb9b7e55 100644 (file)
@@ -26,7 +26,7 @@
 (* $Id$ *)
 
 type thingsToInitilaize = 
-  ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
+  ConfigurationFile | Db | Environment | Getter | CmdLine | Registry
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -45,16 +45,13 @@ let conffile = ref BuildTimeConf.matita_conf
 let registry_defaults = [
   "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.verbose",              "false";
   "matita.paste_unicode_as_tex", "false";
   "matita.noinnertypes",         "false";
   "matita.do_heavy_checks",      "true";
-    (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
-     * intuitively verbose *)
+  "matita.moo",                  "true";
 ]
 
 let set_registry_values =
@@ -105,16 +102,6 @@ let initialize_db init_status =
   else
     init_status
 
-let initialize_makelib init_status = 
-  wants [ConfigurationFile] init_status;
-  if not (already_configured [Makelib] init_status) then
-    begin
-      MatitamakeLib.initialize (); 
-      Makelib::init_status
-    end
-  else
-    init_status
-
 let initialize_environment init_status = 
   wants [CmdLine] init_status;
   if not (already_configured [Getter;Environment] init_status) then
@@ -139,76 +126,29 @@ let _ =
   List.iter
     (fun (name, s) -> Hashtbl.replace usages name s)
     [ "matitac", 
-        Printf.sprintf "MatitaC v%s
+        Printf.sprintf "Matita batch compiler v%s
 Usage: matitac [ OPTION ... ] FILE
 Options:"
           BuildTimeConf.version;
-      "gragrep",
-        Printf.sprintf "Grafite Grep v%s
-Usage: gragrep [ -r ] PATH
-Options:"
-          BuildTimeConf.version;
-      "matitaprover",
-        Printf.sprintf "Matita's prover v%s
+        "matitaprover",
+        Printf.sprintf "Matita (TPTP) prover v%s
 Usage: matitaprover [ -tptppath ] FILE.p
 Options:"
           BuildTimeConf.version;
       "matita",
-        Printf.sprintf "Matita v%s
-Usage: matita [ OPTION ... ] [ FILE ... ]
-Options:"
-          BuildTimeConf.version;
-      "cicbrowser",
-        Printf.sprintf
-          "CIC Browser v%s
-Usage: cicbrowser [ URL | WHELP QUERY ]
+        Printf.sprintf "Matita interactive theorem prover v%s
+Usage: matita [ OPTION ... ] [ FILE ]
 Options:"
           BuildTimeConf.version;
       "matitadep",
-        Printf.sprintf "MatitaDep v%s
-Usage: matitadep [ OPTION ... ] FILE ...
+        Printf.sprintf "Matita depency file generator v%s
+Usage: matitadep [ OPTION ... ] 
 Options:"
           BuildTimeConf.version;
       "matitaclean",
         Printf.sprintf "MatitaClean v%s
 Usage: matitaclean all
-       matitaclean [ (FILE | URI) ... ]
-Options:"
-          BuildTimeConf.version;
-      "matitamake",
-        Printf.sprintf "MatitaMake v%s
-Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
-  init
-    Parameters: name (the name of the development, required)
-                root (the directory in which the delopment is rooted, 
-                      optional, default is current working directory)
-    Description: tells matitamake that a new development radicated 
-      in the current working directory should be handled.
-  clean
-    Parameters: name (the name of the development to destroy, optional)
-      If omitted the development that holds the current working 
-      directory is used (if any).
-    Description: clean the develpoment.
-  list
-    Parameters: 
-    Description: lists the known developments and their roots.
-  destroy
-    Parameters: name (the name of the development to destroy, required)
-    Description: deletes a development (only from matitamake metadat, no
-      .ma files will be deleted).
-  build
-    Parameters: name (the name of the development to build, required)
-    Description: completely builds the develpoment.
-  publish
-    Parameters: name (the name of the development to publish, required)
-    Description: cleans the development in the user space, rebuilds it
-      in the system space ('ro' repositories, that for this operation 
-      becames writable). 
-Notes:
-  If target is omitted an 'all' will be used as the default.
-  With -build you can build a development wherever it is.
-  If you specify a target it implicitly refers to the development that
-  holds the current working directory (if any).
+       matitaclean ( FILE | URI )
 Options:"
           BuildTimeConf.version;
     ]
@@ -231,23 +171,16 @@ let parse_cmdline init_status =
     wants [Registry] init_status;
     let includes = ref [] in
     let default_includes = [ 
-      ".";
       BuildTimeConf.stdlib_dir_devel;
       BuildTimeConf.stdlib_dir_installed ; ] 
     in
     let absolutize s =
-      if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s
+      if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
     in
     let args = ref [] in
     let add_l l = fun s -> l := s :: !l in
-    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" true in
     let set_baseuri s =
@@ -277,18 +210,13 @@ let parse_cmdline init_status =
         "-profile-only",
           Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
           "Activates only profiler with label matching the provided regex";
-        "-bench", 
-          Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
-          "Turns on parsable output on stdout, that is timings for matitac...";
-        "-preserve",
-          Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
-          "Turns off automatic baseuri cleaning";
-        "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
         "-system", Arg.Unit (fun () ->
               Helm_registry.set_bool "matita.system" true),
             ("Act on the system library instead of the user one"
              ^ "\n    WARNING: not for the casual user");
-        "-v", Arg.Unit increase_verbosity, "Increase verbosity";
+        "-v", 
+          Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
+          "Verbose mode";
         "--version", Arg.Unit print_version, "Prints version";
       ] in
       let debug_arg_spec =
@@ -335,18 +263,12 @@ let conf_components =
   [ load_configuration; fill_registry; parse_cmdline]
 
 let other_components =
-  [ initialize_makelib; initialize_db; initialize_environment ]
+  [ initialize_db; initialize_environment ]
 
 let initialize_all () =
   status := 
     List.fold_left (fun s f -> f s) !status
     (conf_components @ other_components)
-(*     initialize_notation 
-      (initialize_environment 
-        (initialize_db 
-          (initialize_makelib
-            (load_configuration
-              (parse_cmdline !status))))) *)
 
 let parse_cmdline_and_configuration_file () =
   status := List.fold_left (fun s f -> f s) !status conf_components