Merge branch 'reload_libraries' into 'master'

graphical interfaces now reload libraries when doing reload

See merge request !217

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)

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.
 
  *)
 

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 =