Commit 3a3014de authored by Sylvain Dailler's avatar Sylvain Dailler

Controller_itp.reload_files/add_file now raises parse/type errors

It formerly returned them.
Also, removes dead commented code.
parent 6564ad92
......@@ -71,14 +71,14 @@ let controller = Controller_itp.create_controller config env session
(* adds a file in the new session *)
let file : Session_itp.file =
let file_name = "examples/logic/hello_proof.why" in
let errors = Controller_itp.add_file controller file_name in
match errors with
| None ->
Session_itp.get_file session file_name
| Some e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name
Exn_printer.exn_printer e;
exit 1
try
Controller_itp.add_file controller file_name;
Session_itp.get_file session file_name
with
| Controller_itp.Errors_list le ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name
(Pp.print_list Pp.space Exn_printer.exn_printer) le;
exit 1
(* explore the theories in that file *)
let theories = Session_itp.file_theories file
......
......@@ -234,14 +234,15 @@ let reload_files (c : controller) ~use_shapes =
Whyconf.Hprover.reset c.controller_provers;
load_drivers c;
c.controller_session <- empty_session ~from:old_ses (get_dir old_ses);
(* try
*)
merge_files ~use_shapes c.controller_env c.controller_session old_ses
(* not need_anymore
with e ->
c.controller_session <- old_ses;
raise e
*)
merge_files ~use_shapes c.controller_env c.controller_session old_ses
exception Errors_list of exn list
let reload_files (c: controller) ~use_shapes =
let errors, b1, b2 = reload_files c ~use_shapes in
match errors with
| [] -> b1, b2
| _ -> raise (Errors_list errors)
let add_file c ?format fname =
let file_is_detached,theories,errors =
......@@ -251,7 +252,11 @@ let add_file c ?format fname =
let (_ : file) = add_file_section c.controller_session fname ~file_is_detached theories format in
errors
let add_file c ?format fname =
let errors = add_file c ?format fname in
match errors with
| None -> ()
| Some error -> raise (Errors_list [error])
module type Scheduler = sig
val blocking: bool
......
......@@ -106,8 +106,9 @@ val print_session : Format.formatter -> controller -> unit
exception Errors_list of exn list
val reload_files : controller -> use_shapes:bool -> exn list * bool * bool
val reload_files : controller -> use_shapes:bool -> bool * bool
(** reload the files of the given session:
- each file is parsed again and theories/goals extracted from it. If
......@@ -152,17 +153,18 @@ val reload_files : controller -> use_shapes:bool -> exn list * bool * bool
it, neither to its subgoals.
[reload_files] It returns a triple (e, o, d): o true means there are
[reload_files] It returns a pair (o, d): o true means there are
obsolete goals, d means there are missed objects (goals, transformations,
theories or files) that are now detached in the session returned.
[e] is the list of parsing of typing errors
If parsing or typing errors occurs, a list of errors is raised inside
exception Errors_list.
*)
val add_file : controller -> ?format:Env.fformat -> string -> exn option
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont].
parsing or typing errors are signaled by a non-none result
parsing or typing errors are raised inside exception Errors_list
*)
val remove_subtree: notification:notifier -> removed:notifier ->
......
......@@ -587,14 +587,15 @@ end
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
capture_parse_or_type_errors
(fun c -> let (e,_,_) = reload_files ~use_shapes c in e) cont
(fun c ->
try let (_,_) = reload_files ~use_shapes c in [] with
| Errors_list le -> le) cont
let add_file cont ?format fname =
capture_parse_or_type_errors
(fun c ->
match add_file c ?format fname with
| None -> []
| Some e -> [e]) cont
try add_file c ?format fname; [] with
| Errors_list le -> le) cont
(* ----------------------------------- ------------------------------------- *)
......
......@@ -53,59 +53,6 @@ let get_session_dir ~allow_mkdir files =
dir
(******************************)
(* Creation of the controller *)
(******************************)
(* [cont_from_session]: returns an option to a boolean which returns None in
case of failure, true if nothing is left to do and false if sessions was
loaded but [f] should still be added to the session as a file. *)
(*
let cont_from_session ~notify cont f : bool option =
(* If a file is given, find the corresponding directory *)
let dir = try (Filename.chop_extension f) with
| Invalid_argument _ -> f in
(* create project directory if needed *)
if Sys.file_exists dir then
begin
(* Case of user giving a file that gets chopped to an other file *)
if not (Sys.is_directory dir) then
begin
Format.eprintf "Not a directory: %s@." dir;
exit 1
end
end
else
begin
Format.dprintf debug "'%s' does not exist. \
Creating directory of that name for the Why3 session@." dir;
Unix.mkdir dir 0o777
end;
(* we load the session *)
let ses,use_shapes = load_session dir in
Format.dprintf debug "using shapes: %b@." use_shapes;
(* temporary, this should not be donne like this ! *)
Controller_itp.set_session cont ses;
(* update the session *)
try (Controller_itp.reload_files cont ~use_shapes;
(* Check if the initial file given was a file or not. If it was, we return
that it should be added to the session. *)
if Sys.file_exists f && not (Sys.is_directory f) then
Some false
else
Some true) with
| e ->
begin
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
notify (Message (Parse_Or_Type_Error s));
None
end
*)
(******************)
(* Simple queries *)
(******************)
......
......@@ -350,15 +350,14 @@ let () =
let ses,use_shapes = S.load_session dir in
let cont = Controller_itp.create_controller config env ses in
(* update the session *)
let errors, found_obs, found_detached =
Controller_itp.reload_files cont ~use_shapes;
let found_obs, found_detached =
try
Controller_itp.reload_files cont ~use_shapes
with
| Controller_itp.Errors_list l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
exit 1
in
begin match errors with
| [] -> ()
| l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
exit 1
end;
Debug.dprintf debug " done.@.";
if !opt_obsolete_only && not (found_detached || found_obs)
then
......
......@@ -88,16 +88,14 @@ let read_update_session ~allow_obsolete env config fname =
S.update_session ~ctxt session env config
*)
let cont = Controller_itp.create_controller config env session in
let errors, found_obs, some_merge_miss =
Controller_itp.reload_files cont ~use_shapes
let found_obs, some_merge_miss =
try
Controller_itp.reload_files cont ~use_shapes
with
| Controller_itp.Errors_list l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
exit 1
in
begin
match errors with
| [] -> ()
| l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
exit 1
end;
if (found_obs || some_merge_miss) && not allow_obsolete then raise Exit;
cont, found_obs, some_merge_miss
......
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