1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 type thingsToInitilaize =
29 ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
31 exception FailedToInitialize of thingsToInitilaize
36 if not (List.exists (fun x -> x = item) l) then
37 raise (FailedToInitialize item))
40 let already_configured s l =
41 List.for_all (fun item -> List.exists (fun x -> x = item) l) s
43 let load_configuration init_status =
44 if not (already_configured [ConfigurationFile] init_status) then
46 Helm_registry.load_from BuildTimeConf.matita_conf;
47 ConfigurationFile::init_status
52 let initialize_db init_status =
53 wants [ ConfigurationFile; CmdLine ] init_status;
54 if not (already_configured [ Db ] init_status) then
56 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
57 MatitaDb.create_owner_environment ();
63 let initialize_makelib init_status =
64 wants [ConfigurationFile] init_status;
65 if not (already_configured [Makelib] init_status) then
67 MatitamakeLib.initialize ();
73 let initialize_notation init_status =
74 wants [ConfigurationFile] init_status;
75 if not (already_configured [Notation] init_status) then
77 CicNotation.load_notation BuildTimeConf.core_notation_script;
83 let initialize_environment init_status =
84 wants [ConfigurationFile] init_status;
85 if not (already_configured [Getter;Environment] init_status) then
88 CicEnvironment.set_trust (* environment trust *)
89 (let trust = Helm_registry.get_bool "matita.environment_trust" in
91 Getter::Environment::init_status
98 let usages = Hashtbl.create 11
101 (fun (name, s) -> Hashtbl.replace usages name s)
104 Usage: matitac [ OPTION ... ] FILE
106 BuildTimeConf.version;
109 Usage: matita [ OPTION ... ] [ FILE ... ]
111 BuildTimeConf.version;
115 Usage: cicbrowser [ URL | WHELP QUERY ]
117 BuildTimeConf.version;
119 sprintf "MatitaDep v%s
120 Usage: matitadep [ OPTION ... ] FILE ...
122 BuildTimeConf.version;
124 sprintf "MatitaClean v%s
125 Usage: matitaclean all
126 matitaclean [ (FILE | URI) ... ]
128 BuildTimeConf.version;
131 sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
134 let basename = Filename.basename Sys.argv.(0) in
136 try Filename.chop_extension basename with Invalid_argument _ -> basename
138 try Hashtbl.find usages usage_key with Not_found -> default_usage
140 let registry_defaults =
143 "matita.debug", "false";
144 "matita.external_editor", "gvim -f -c 'go %p' %f";
145 "matita.preserve", "false";
146 "matita.quiet", "false";
149 let set_registry_values =
150 List.iter (fun key, value -> Helm_registry.set ~key ~value)
152 let parse_cmdline init_status =
153 if not (already_configured [CmdLine] init_status) then begin
154 let includes = ref [] in
156 let add_l l = fun s -> l := s :: !l in
159 "-I", Arg.String (add_l includes),
160 ("<path> Adds path to the list of searched paths for the "
161 ^ "include command");
162 "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true),
163 "Turn off verbose compilation";
165 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
166 "Turns off automatic baseuri cleaning";
167 "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
168 ("Avoid using external database connection "
169 ^ "(WARNING: disable many features)");
172 if BuildTimeConf.debug then
174 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
175 ("Do not catch top-level exception "
176 ^ "(useful for backtrace inspection)");
180 std_arg_spec @ debug_arg_spec
182 let set_list ~key l =
183 Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)
185 set_registry_values registry_defaults;
186 Arg.parse arg_spec (add_l args) (usage ());
187 set_list ~key:"matita.includes" includes;
188 set_list ~key:"matita.args" args;
189 CmdLine :: init_status
194 print_endline (usage ());
197 let initialize_all () =
199 List.fold_left (fun s f -> f s) !status
200 [ parse_cmdline; load_configuration; initialize_makelib;
201 initialize_db; initialize_environment; initialize_notation ]
202 (* initialize_notation
203 (initialize_environment
207 (parse_cmdline !status))))) *)
209 let load_configuration_file () =
210 status := load_configuration !status
212 let initialize_notation () =
213 status := initialize_notation (load_configuration !status)
215 let parse_cmdline () =
216 status := parse_cmdline !status