λδ site update

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

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 5ca8ffc82a7f6f600303c41fe0d3c32afa6f6cbd..70125f54c222bb5dc3c3d146a8a7cc8aecfee294 100644 (file)
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -25,10 +25,10 @@
 
 (* $Id$ *)
 
-type thingsToInitilaize = 
+type thingsToInitialize = 
   ConfigurationFile | Db | Environment | Getter | CmdLine | Registry
   
-exception FailedToInitialize of thingsToInitilaize
+exception FailedToInitialize of thingsToInitialize
 
 let wants s l = 
   List.iter (
@@ -54,6 +54,7 @@ let registry_defaults = [
   "matita.do_heavy_checks",      "true";
   "matita.moo",                  "true";
   "matita.extract",              "false";
+  "matita.execcomments",         "false";
 ]
 
 let set_registry_values =
@@ -175,7 +176,10 @@ let parse_cmdline init_status =
     let includes = ref [] in
     let default_includes = [ 
       BuildTimeConf.stdlib_dir_devel;
-      BuildTimeConf.stdlib_dir_installed ; ] 
+      BuildTimeConf.stdlib_dir_installed ; 
+      BuildTimeConf.new_stdlib_dir_devel;
+      BuildTimeConf.new_stdlib_dir_installed ; 
+    ] 
     in
     let absolutize s =
       if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
@@ -192,6 +196,8 @@ let parse_cmdline init_status =
           (HExtlib.normalize_path (absolutize path)^" "^uri)
       | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
     in
+    let no_default_includes = ref false in
+    let execcomments = ref false in
     let arg_spec =
       let std_arg_spec = [
         "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
@@ -217,10 +223,14 @@ let parse_cmdline init_status =
               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", 
+        "-no-default-includes", Arg.Set no_default_includes,
+          "Do not include the default searched paths for the include command"; 
+        "-execcomments", Arg.Set execcomments,
+          "Execute the content of (** ... *) comments";
+       "-v", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
           "Verbose mode";
-        "--version", Arg.Unit print_version, "Prints version";
+        "--version", Arg.Unit print_version, "Prints version"
       ] in
       let debug_arg_spec =
         if BuildTimeConf.debug then
@@ -229,7 +239,7 @@ let parse_cmdline init_status =
               ("Do not catch top-level exception "
               ^ "(useful for backtrace inspection)");
            "-onepass",
-           Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
+           Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true),
            "Enable only one disambiguation pass";    
           ]
         else []
@@ -240,6 +250,8 @@ let parse_cmdline init_status =
       Helm_registry.set_list Helm_registry.of_string ~key ~value:l
     in
     Arg.parse arg_spec (add_l args) (usage ());
+    Helm_registry.set_bool ~key:"matita.execcomments" ~value:!execcomments;
+    let default_includes = if !no_default_includes then [] else default_includes in
     let includes = 
       List.map (fun x -> HExtlib.normalize_path (absolutize x)) 
        ((List.rev !includes) @ default_includes) 
@@ -271,7 +283,8 @@ let other_components =
 let initialize_all () =
   status := 
     List.fold_left (fun s f -> f s) !status
-    (conf_components @ other_components)
+    (conf_components @ other_components);
+  NCicLibrary.init ()
 
 let parse_cmdline_and_configuration_file () =
   status := List.fold_left (fun s f -> f s) !status conf_components
@@ -280,4 +293,8 @@ let initialize_environment () =
   status := initialize_environment !status
 
 let _ =
-  Inversion_principle.init ()
+  CicFix.init ();
+  Inversion_principle.init ();
+  CicRecord.init ();
+  CicElim.init ()
+;;