(* $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 (
let registry_defaults = [
"matita.debug", "false";
+ "matita.debug_menu", "false";
"matita.external_editor", "gvim -f -c 'go %p' %f";
"matita.profile", "true";
"matita.system", "false";
"matita.noinnertypes", "false";
"matita.do_heavy_checks", "true";
"matita.moo", "true";
+ "matita.extract", "false";
+ "matita.execcomments", "false";
]
let set_registry_values =
try Hashtbl.find usages usage_key with Not_found -> default_usage
;;
-let dump f =
- let module G = GrafiteAst in
- let module L = LexiconAst in
- let module H = HExtlib in
- Helm_registry.set_bool "matita.moo" false;
- let floc = H.dummy_floc in
- let nl_ast = G.Comment (floc, G.Note (floc, "")) in
- let och = open_out f in
- let atexit () = close_out och in
- let out_comment och s =
- let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in
- Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
- in
- let out_line_comment och s =
- let l = 70 - String.length s in
- let s = Printf.sprintf " %s %s" s (String.make l '*') in
- out_comment och s
- in
- let out_preamble och (path, lines) =
- let ich = open_in path in
- let rec print i =
- if i > 0 then
- let s = input_line ich in
- begin Printf.fprintf och "%s\n" s; print (pred i) end
- in
- print lines;
- out_line_comment och "This file was automatically generated: do not edit"
- in
- let pp_ast_statement st =
- GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- ~lazy_term_pp:CicNotationPp.pp_term
- ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
- in
- let nl () = output_string och (pp_ast_statement nl_ast) in
- let rt_base_dir = Filename.dirname Sys.argv.(0) in
- let path = Filename.concat rt_base_dir "matita.ma.templ" in
- let lines = 14 in
- out_preamble och (path, lines);
- let grafite_parser_cb fname =
- let ast = G.Executable
- (floc, G.Command (floc, G.Include (floc, fname))) in
- output_string och (pp_ast_statement ast); nl (); nl ()
- in
- let matita_engine_cb = function
- | G.Executable (_, G.Macro (_, G.Inline _))
- | G.Executable (_, G.Command (_, G.Include _)) -> ()
- | ast ->
- output_string och (pp_ast_statement ast); nl (); nl ()
- in
- let matitac_lib_cb = output_string och in
- GrafiteParser.set_callback grafite_parser_cb;
- MatitaEngine.set_callback matita_engine_cb;
- MatitacLib.set_callback matitac_lib_cb;
- at_exit atexit
-;;
-
let extra_cmdline_specs = ref []
let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
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 ()
+;;
projects / helm.git / blobdiff