X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=70125f54c222bb5dc3c3d146a8a7cc8aecfee294;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=cf96c5ba1261e45a29c0396bd1c1c6778d326016;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index cf96c5ba1..70125f54c 100644 --- 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 ( @@ -44,6 +44,7 @@ let conffile = ref BuildTimeConf.matita_conf 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"; @@ -52,6 +53,8 @@ let registry_defaults = [ "matita.noinnertypes", "false"; "matita.do_heavy_checks", "true"; "matita.moo", "true"; + "matita.extract", "false"; + "matita.execcomments", "false"; ] let set_registry_values = @@ -164,64 +167,6 @@ let usage () = 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 @@ -231,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 @@ -248,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, " forces the baseuri of path"; @@ -273,12 +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"); - "-dump", Arg.String dump, - " Dump with expanded macros to "; - "-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 @@ -287,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 [] @@ -298,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) @@ -329,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 @@ -338,4 +293,8 @@ let initialize_environment () = status := initialize_environment !status let _ = - Inversion_principle.init () + CicFix.init (); + Inversion_principle.init (); + CicRecord.init (); + CicElim.init () +;;