(* $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 (
"matita.do_heavy_checks", "true";
"matita.moo", "true";
"matita.extract", "false";
+ "matita.execcomments", "false";
]
let set_registry_values =
let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
let parse_cmdline init_status =
- let dump fname =
- let atexit = MatitacLib.dump fname in
- at_exit atexit
- in
if not (already_configured [CmdLine] init_status) then begin
wants [Registry] 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
(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";
Helm_registry.set_bool "matita.system" true),
("Act on the system library instead of the user one"
^ "\n WARNING: not for the casual user");
- "-dump", Arg.String dump,
- "<filename> Dump with expanded macros to <filename>";
- "-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
("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 []
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)
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
status := initialize_environment !status
let _ =
- Inversion_principle.init ()
+ CicFix.init ();
+ Inversion_principle.init ();
+ CicRecord.init ();
+ CicElim.init ()
+;;