Commit 59c59389 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix a few issues with option handling.

parent f44ea070
......@@ -32,6 +32,7 @@ let common_options = [
let initialize options default usage =
Arg.parse (Arg.align (List.append options common_options)) default usage;
if Debug.Args.option_list () then exit 0;
let config = Whyconf.read_config !opt_config in
let config = List.fold_left Whyconf.merge_config config !opt_extra in
let main = Whyconf.get_main config in
......@@ -39,3 +40,7 @@ let initialize options default usage =
Debug.Args.set_flags_selected ();
let lp = List.rev_append !opt_loadpath (Whyconf.loadpath main) in
(Env.create_env lp, config)
let exit_with_usage options usage =
Arg.usage (Arg.align (List.append options common_options)) usage;
exit 1
......@@ -13,3 +13,5 @@ open Why3
val initialize : (string * Arg.spec * string) list ->
(string -> unit) -> string -> Env.env * Whyconf.config
val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a
......@@ -72,8 +72,9 @@ let command_path =
| Some p -> Filename.concat p "bin"
| None -> Filename.concat Config.libdir "commands"
let command cmd =
let cmd = Filename.concat command_path ("why3" ^ cmd) in
let command scmd =
let scmd = "why3" ^ scmd in
let cmd = Filename.concat command_path scmd in
if not (Sys.file_exists cmd) then begin
printf "'%s' is not a why3 command.@." cmd;
exit 1
......@@ -84,7 +85,7 @@ let command cmd =
for i = !Arg.current + 1 to Array.length Sys.argv - 1 do
args := Sys.argv.(i) :: !args;
done;
Unix.execv cmd (Array.of_list (("why3" ^ cmd) :: List.rev !args))
Unix.execv cmd (Array.of_list (scmd :: List.rev !args))
let () = try
Arg.parse option_list command usage_msg;
......
......@@ -41,10 +41,7 @@ let (env, config) =
Args.initialize option_list add_opt usage_msg
let () =
if !opt_file = None then begin
Arg.usage option_list usage_msg;
exit 1
end
if !opt_file = None then Args.exit_with_usage option_list usage_msg
let do_input f =
let fname, cin =
......
......@@ -75,10 +75,8 @@ let (env, config) =
Args.initialize option_list add_opt_file usage_msg
let () =
if Queue.is_empty opt_queue then begin
Arg.usage option_list usage_msg;
exit 1
end
if Queue.is_empty opt_queue then
Args.exit_with_usage option_list usage_msg
let opt_output =
match !opt_output with
......
......@@ -147,10 +147,7 @@ let (env, config) =
Args.initialize option_list add_opt_file usage_msg
let () = try
if Queue.is_empty opt_queue then begin
Arg.usage option_list usage_msg;
exit 1
end;
if Queue.is_empty opt_queue then Args.exit_with_usage option_list usage_msg;
if !opt_prover <> None && !opt_driver <> None then begin
eprintf "Options '-P'/'--prover' and \
......
......@@ -64,10 +64,7 @@ let (env, config) =
Args.initialize option_list add_opt_file usage_msg
let () =
if Queue.is_empty opt_queue then begin
Arg.usage option_list usage_msg;
exit 1
end
if Queue.is_empty opt_queue then Args.exit_with_usage option_list usage_msg
let opt_output =
match !opt_output with
......
......@@ -105,7 +105,7 @@ let (env, config) =
let fname =
match !opt_file with
| None -> Arg.usage option_list usage_msg; exit 1
| None -> Args.exit_with_usage option_list usage_msg
| Some f -> f
let found_upgraded_prover = ref false
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment