Commit 45ec32e6 authored by Sylvain's avatar Sylvain

graphical interfaces now reload libraries when doing reload

After 11f28a8a, why3ide would not reload dependency libraries when
reloading a file. This implements 2 modes for reload_files:
- reload with libraries and drivers (intended for IDEs and graphical
interfaces)
- reload only the current file (intended to optimize Why3 used in scripts
files)
parent 6f78158e
......@@ -240,17 +240,25 @@ let print_session fmt c =
(** reload files, associating old proof attempts and transformations
to the new goals. old theories and old goals for which we cannot
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
tasks associated to them.
When [hard_reload] option is true, dependencies and drivers are also
reloaded.
*)
let reload_files (c : controller) ~shape_version =
let reload_files ?(hard_reload=false) (c : controller) ~shape_version =
let old_ses = c.controller_session in
if hard_reload then begin
c.controller_env <- Env.create_env (Env.get_loadpath c.controller_env);
Whyconf.Hprover.reset c.controller_provers;
load_drivers c;
end;
c.controller_session <- empty_session ~shape_version ~from:old_ses (get_dir old_ses);
merge_files ~shape_version c.controller_env c.controller_session old_ses
exception Errors_list of exn list
let reload_files (c: controller) ~shape_version =
let errors, b1, b2 = reload_files c ~shape_version in
let reload_files ?(hard_reload=false) (c: controller) ~shape_version =
let errors, b1, b2 = reload_files c ~shape_version ~hard_reload in
match errors with
| [] -> b1, b2
| _ -> raise (Errors_list errors)
......
......@@ -122,7 +122,8 @@ val print_session : Format.formatter -> controller -> unit
exception Errors_list of exn list
val reload_files : controller -> shape_version:int option -> bool * bool
val reload_files : ?hard_reload:bool -> controller ->
shape_version:int option -> bool * bool
(** [reload_files] 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
......@@ -175,6 +176,8 @@ val reload_files : controller -> shape_version:int option -> bool * bool
proof attempts and transformations, but no task is associated to
it, neither to its subgoals.
When the option [hard_reload] is true (false by default), libraries and
drivers are also reloaded.
*)
......
......@@ -627,9 +627,10 @@ end
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~shape_version =
let hard_reload = true in
capture_parse_or_type_errors
(fun c ->
try let (_,_) = reload_files ~shape_version c in [] with
try let (_,_) = reload_files ~hard_reload ~shape_version c in [] with
| Errors_list le -> le) cont
let add_file cont ?format fname =
......
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