From 65e37d3f202b99ea45b36565a724805e8d925175 Mon Sep 17 00:00:00 2001 From: Sylvain Date: Tue, 20 Aug 2019 10:59:36 +0200 Subject: [PATCH] graphical interfaces now reload libraries when doing reload After 11f28a8a62, 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) --- src/session/controller_itp.ml | 16 ++++++++++++---- src/session/controller_itp.mli | 5 ++++- src/session/itp_server.ml | 3 ++- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index 94d46e6c4..92ec1e425 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -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) diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli index 799375aed..62ee50aa3 100644 --- a/src/session/controller_itp.mli +++ b/src/session/controller_itp.mli @@ -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. *) diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 789dba0ab..f366a63d5 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -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 = -- GitLab