Commit 6b88767e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'itp' into itp_new_why3session

parents cbad94c7 0fc3a92d
...@@ -31,7 +31,7 @@ let debug = Debug.register_info_flag ...@@ -31,7 +31,7 @@ let debug = Debug.register_info_flag
let () = Debug.set_flag debug let () = Debug.set_flag debug
let opt_file = ref None let files = Queue.create ()
(* (*
let opt_stats = ref true let opt_stats = ref true
*) *)
...@@ -106,19 +106,10 @@ let option_list = [ ...@@ -106,19 +106,10 @@ let option_list = [
Arg.Unit (fun () -> Debug.unset_flag debug), Arg.Unit (fun () -> Debug.unset_flag debug),
" same as -q") ] " same as -q") ]
let add_opt_file f = match !opt_file with let add_file f = Queue.push f files
| Some _ ->
raise (Arg.Bad "only one parameter")
| None ->
opt_file := Some f
let config, _, env = let config, _, env =
Whyconf.Args.initialize option_list add_opt_file usage_msg Whyconf.Args.initialize option_list add_file usage_msg
let fname =
match !opt_file with
| None -> Whyconf.Args.exit_with_usage option_list usage_msg
| Some f -> f
let found_upgraded_prover = ref false let found_upgraded_prover = ref false
...@@ -341,9 +332,18 @@ let run_as_bench env_session = ...@@ -341,9 +332,18 @@ let run_as_bench env_session =
let () = let () =
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:false files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage option_list usage_msg
in
if not (Queue.is_empty files) then
Whyconf.Args.exit_with_usage option_list usage_msg;
try try
Debug.dprintf debug "Opening session...@?"; Debug.dprintf debug "Opening session '%s'...@?" dir;
let ses,use_shapes = S.load_session project_dir in let ses,use_shapes = S.load_session dir in
let cont = Controller_itp.create_controller config env ses in let cont = Controller_itp.create_controller config env ses in
(* update the session *) (* update the session *)
let found_obs, some_merge_miss = let found_obs, some_merge_miss =
...@@ -379,7 +379,7 @@ let () = ...@@ -379,7 +379,7 @@ let () =
with with
| e when not (Debug.test_flag Debug.stack_trace) -> | e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "Error while opening session with database '%s' : %a@." eprintf "Error while opening session with database '%s' : %a@."
project_dir dir
Exn_printer.exn_printer e; Exn_printer.exn_printer e;
eprintf "Aborting...@."; eprintf "Aborting...@.";
exit 1 exit 1
......
Supports Markdown
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