Commit 65e37d3f authored by Sylvain's avatar Sylvain Committed by MARCHE Claude

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 4bb6cff4
...@@ -240,17 +240,25 @@ let print_session fmt c = ...@@ -240,17 +240,25 @@ let print_session fmt c =
(** reload files, associating old proof attempts and transformations (** reload files, associating old proof attempts and transformations
to the new goals. old theories and old goals for which we cannot to the new goals. old theories and old goals for which we cannot
find a corresponding new theory resp. old goal are kept, with 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 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); 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 merge_files ~shape_version c.controller_env c.controller_session old_ses
exception Errors_list of exn list exception Errors_list of exn list
let reload_files (c: controller) ~shape_version = let reload_files ?(hard_reload=false) (c: controller) ~shape_version =
let errors, b1, b2 = reload_files c ~shape_version in let errors, b1, b2 = reload_files c ~shape_version ~hard_reload in
match errors with match errors with
| [] -> b1, b2 | [] -> b1, b2
| _ -> raise (Errors_list errors) | _ -> raise (Errors_list errors)
......
...@@ -122,7 +122,8 @@ val print_session : Format.formatter -> controller -> unit ...@@ -122,7 +122,8 @@ val print_session : Format.formatter -> controller -> unit
exception Errors_list of exn list 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 (** [reload_files] returns a pair [(o,d)]: [o] true means there are
obsolete goals, [d] means there are missed objects (goals, obsolete goals, [d] means there are missed objects (goals,
transformations, theories or files) that are now detached in the transformations, theories or files) that are now detached in the
...@@ -175,6 +176,8 @@ val reload_files : controller -> shape_version:int option -> bool * bool ...@@ -175,6 +176,8 @@ val reload_files : controller -> shape_version:int option -> bool * bool
proof attempts and transformations, but no task is associated to proof attempts and transformations, but no task is associated to
it, neither to its subgoals. 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 ...@@ -627,9 +627,10 @@ end
(* Reload_files that is used even if the controller is not correct. It can (* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *) be incorrect and end up in a correct state. *)
let reload_files cont ~shape_version = let reload_files cont ~shape_version =
let hard_reload = true in
capture_parse_or_type_errors capture_parse_or_type_errors
(fun c -> (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 | Errors_list le -> le) cont
let add_file cont ?format fname = 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