- added support for "-nodb" flag (still missing support for matitaclean which relies...

[helm.git] / helm / matita / matitaInit.ml

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index aab81560169be0fba37495ffeeb8994e053e0a23..f7003796b4027e25d140fedbb4b74d19806a8a8a 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -23,9 +23,11 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 type thingsToInitilaize = 
   ConfigurationFile | Db | Environment | Getter | Notation | 
-  Paramodulation | Makelib
+  Paramodulation | Makelib | CmdLine
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -49,8 +51,8 @@ let load_configuration init_status =
     init_status
 
 let initialize_db init_status = 
-  wants [ConfigurationFile] init_status;
-  if not (already_configured [Db] init_status) then
+  wants [ ConfigurationFile; CmdLine ] init_status;
+  if not (already_configured [ Db ] init_status) then
     begin
       MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
       MatitaDb.create_owner_environment ();
@@ -103,7 +105,105 @@ let initialize_environment init_status =
     init_status 
   
 let status = ref []
-    
+
+let usages = Hashtbl.create 11
+let _ =
+  List.iter
+    (fun (name, s) -> Hashtbl.replace usages name s)
+    [ "matitac", 
+        sprintf "MatitaC v%s
+Usage: matitac [ OPTION ... ] FILE
+Options:"
+          BuildTimeConf.version;
+      "matita",
+        sprintf "Matita v%s
+Usage: matita [ OPTION ... ] [ FILE ... ]
+Options:"
+          BuildTimeConf.version;
+      "cicbrowser",
+        sprintf
+          "CIC Browser v%s
+Usage: cicbrowser [ URL | WHELP QUERY ]
+Options:"
+          BuildTimeConf.version;
+      "matitadep",
+        sprintf "MatitaDep v%s
+Usage: matitadep [ OPTION ... ] FILE ...
+Options:"
+          BuildTimeConf.version;
+      "matitaclean",
+        sprintf "MatitaClean v%s
+Usage: matitaclean all
+       matitaclean [ (FILE | URI) ... ]
+Options:"
+          BuildTimeConf.version;
+    ]
+let default_usage =
+  sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
+
+let usage () =
+  let basename = Filename.basename Sys.argv.(0) in
+  let usage_key =
+    try Filename.chop_extension basename with Invalid_argument  _ -> basename
+  in
+  try Hashtbl.find usages usage_key with Not_found -> default_usage
+
+let registry_defaults =
+  [ "matita.debug", "false";
+    "matita.quiet", "false";
+    "matita.preserve", "false";
+    "db.nodb", "false";
+  ]
+
+let set_registry_values =
+  List.iter (fun key, value -> Helm_registry.set ~key ~value)
+
+let parse_cmdline init_status =
+  if not (already_configured [CmdLine] init_status) then begin
+    let includes = ref [] in
+    let args = ref [] in
+    let add_l l = fun s -> l := s :: !l in
+    let arg_spec =
+      let std_arg_spec = [
+        "-I", Arg.String (add_l includes),
+          ("<path> Adds path to the list of searched paths for the "
+           ^ "include command");
+        "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true),
+          "Turn off verbose compilation";
+        "-preserve",
+          Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
+          "Turns off automatic baseuri cleaning";
+        "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
+              ("Avoid using external database connection "
+               ^ "(WARNING: disable many features)");
+      ] in
+      let debug_arg_spec =
+        if BuildTimeConf.debug then
+          [ "-debug",
+            Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
+              ("Do not catch top-level exception "
+              ^ "(useful for backtrace inspection)");
+          ]
+        else []
+      in
+      std_arg_spec @ debug_arg_spec
+    in
+    let set_list ~key l =
+      Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)
+    in
+    set_registry_values registry_defaults;
+    Arg.parse arg_spec (add_l args) (usage ());
+    set_list ~key:"matita.includes" includes;
+    set_list ~key:"matita.args" args;
+Helm_registry.save_to "./foo.conf.xml";
+    CmdLine :: init_status
+  end else
+    init_status
+
+let die_usage () =
+  print_endline (usage ());
+  exit 1
+
 let initialize_all () =
   status := 
     initialize_notation 
@@ -111,11 +211,15 @@ let initialize_all () =
         (initialize_db 
           (initialize_paramodulation 
             (initialize_makelib
-              (load_configuration !status)))))
+              (load_configuration
+                (parse_cmdline !status))))))
 
-let load_config_only () =
+let load_configuration_file () =
   status := load_configuration !status
 
 let initialize_notation () =
   status := initialize_notation (load_configuration !status)
-  
+
+let parse_cmdline () =
+  status := parse_cmdline !status
+