Commit 8abbc30e authored by François Bobot's avatar François Bobot

why3session: better error message for outdated session

parent c54e709a
......@@ -703,7 +703,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
| ProverAmbiguity (config,fp,provers ) ->
fprintf fmt "More than one prover@ in %s@ correspond@ to \"%a\":@ %a@."
(get_conf_file config) print_filter_prover fp
(Pp.print_iter2 Mprover.iter Pp.space Pp.nothing print_prover Pp.nothing)
(Pp.print_iter2 Mprover.iter Pp.comma Pp.nothing print_prover Pp.nothing)
provers
| ParseFilterProver s ->
fprintf fmt
......
......@@ -1755,15 +1755,6 @@ let load_prover eS prover =
let unload_provers eS = PHprover.clear eS.loaded_provers
let () = Exn_printer.register
(fun fmt exn ->
match exn with
| NoTask ->
Format.fprintf fmt
"A goal doesn't contain a task but here it needs one"
| _ -> raise exn)
let ft_of_th th =
let fn = Filename.basename th.theory_parent.file_name in
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
......@@ -2395,6 +2386,19 @@ let key_any = function
| Theory th -> th.theory_key
| Metas ms -> ms.metas_key
let () = Exn_printer.register
(fun fmt exn ->
match exn with
| NoTask ->
Format.fprintf fmt
"A goal doesn't contain a task but here it needs one"
| OutdatedSession ->
Format.fprintf fmt
"The session@ is@ outdated@ (not@ in@ sync@ with@ the@ current@ \
file).@ In@ this@ configuration@ it@ is@ forbidden."
| _ -> raise exn)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
......
......@@ -194,7 +194,12 @@ but@ one@ is@ needed.@.";
end;
(** get the provers *)
let pk = read_to_prover config in
iter_files (run_one ~action env config filters pk)
try
iter_files (run_one ~action env config filters pk)
with OutdatedSession as e ->
eprintf "@.%a@ You@ can@ allow@ it@ with@ the@ option@ -F.@."
Exn_printer.exn_printer e
let cmd_copy =
{ cmd_spec = spec;
......
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