major change (details below): reload is now careful of running provers and focused node

The decision on clearing the whole tree and sending again all nodes
is now completely handled on the itp server side.

- discarded the request Get_Session_Tree_req
- added the notification Reset_whole_tree

Bad side effect: moving to next unproven goal seems working even worse than before

missing feature: reloading when a node is focused should keep the focus
if possible, for now it just unfocus

src/ide/why3_js.ml

@@ -540,6 +540,7 @@ end
 
 let interpNotif (n: notification) =
   match n with
+  | Reset_whole_tree ->  PE.error_print_msg "Reset_whole_tree"
   | Initialized _g ->
       PE.error_print_msg "Initialized"
   | New_node (nid, parent, ntype, name, detached) ->

src/ide/why3ide.ml

@@ -720,10 +720,7 @@ let clear_tree_and_table goals_model =
 (**************)
 
 
-let reload_unsafe () =
-  (* Clearing the tree *)
-  clear_tree_and_table goals_model;
-  send_request Reload_req
+let reload_unsafe () = send_request Reload_req
 
 let save_and_reload () = save_sources (); reload_unsafe ()
 
@@ -1861,19 +1858,12 @@ let () =
       match get_selected_row_references () with
       | [r] ->
           let id = get_node_id r#iter in
-          send_request (Focus_req id);
-          (* TODO not efficient *)
-          clear_tree_and_table goals_model;
-          send_request (Get_Session_Tree_req);
+          send_request (Focus_req id)
       | _ -> print_message ~kind:1 ~mark:"Focus_req error"
                         "Select only one node to perform the focus action");
   connect_menu_item
     unfocus_item
-    ~callback:(fun () ->
-      send_request Unfocus_req;
-      (* TODO not efficient *)
-      clear_tree_and_table goals_model;
-      send_request (Get_Session_Tree_req))
+    ~callback:(fun () -> send_request Unfocus_req)
 
 
 (* the command-line *)
@@ -1881,6 +1871,7 @@ let () =
 let treat_notification n =
   Protocol_why3ide.print_notify_debug n;
   begin match n with
+  | Reset_whole_tree -> clear_tree_and_table goals_model
   | Node_change (id, uinfo)        ->
      begin
        match uinfo with
@@ -1897,7 +1888,12 @@ let treat_notification n =
           in
           if old <> b then begin
               set_status_and_time_column (get_node_row id);
-              if not b then
+              if b then
+                (* Trying to move cursor on first unproven goal around
+             on all cases but not when proofAttempt is updated because
+             ad hoc debugging. *)
+                if_selected_alone id (fun _ -> send_request (Get_first_unproven_node id))
+              else
                 begin
                   try
                     let row = Hint.find node_id_to_gtree id in
@@ -1907,10 +1903,7 @@ let treat_notification n =
                   with Not_found ->
                     Debug.dprintf debug "Warning: no gtk row registered for node %d@." id
                 end
-          end;
-          (* Trying to move cursor on first unproven goal around on all cases
-             but not when proofAttempt is updated because ad hoc debugging. *)
-          send_request (Get_first_unproven_node id)
+          end
        | Proof_status_change (pa, obs, l) ->
           let r = get_node_row id in
           Hint.replace node_id_pa id (pa, obs, l);

src/session/itp_communication.ml

@@ -74,6 +74,7 @@ type update_info =
       * Call_provers.resource_limit
 
 type notification =
+  | Reset_whole_tree
   | New_node     of node_ID * node_ID * node_type * string * bool
   (* Notification of creation of new_node:
      New_node (new_node, parent_node, node_type, name, detached). *)
@@ -113,7 +114,6 @@ type ide_request =
   | Save_file_req           of string * string
   | Get_first_unproven_node of node_ID
   | Mark_obsolete_req       of node_ID
-  | Get_Session_Tree_req
   | Clean_req
   | Save_req
   | Reload_req
@@ -128,5 +128,5 @@ let modify_session (r: ide_request) =
   | Copy_detached _ | Replay_req | Clean_req | Mark_obsolete_req _ -> true
   | Set_config_param _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _
-  | Get_Session_Tree_req | Save_req | Reload_req | Exit_req
+  | Save_req | Reload_req | Exit_req
   | Interrupt_req | Focus_req _ | Unfocus_req -> false

src/session/itp_communication.mli

@@ -80,6 +80,7 @@ type update_info =
       * Call_provers.resource_limit
 
 type notification =
+  | Reset_whole_tree
   | New_node     of node_ID * node_ID * node_type * string * bool
   (** Notification of creation of new_node:
      New_node (new_node, parent_node, node_type, name, detached). *)
@@ -129,7 +130,6 @@ type ide_request =
   (** [Save_file_req(filename, content_of_file)] saves the file *)
   | Get_first_unproven_node of node_ID
   | Mark_obsolete_req       of node_ID
-  | Get_Session_Tree_req
   | Clean_req
   | Save_req
   | Reload_req

src/session/itp_server.ml

@@ -262,7 +262,6 @@ let print_request fmt r =
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
   | Copy_paste _                    -> fprintf fmt "copy paste"
   | Copy_detached _                 -> fprintf fmt "copy detached"
-  | Get_Session_Tree_req            -> fprintf fmt "get session tree"
   | Save_file_req _                 -> fprintf fmt "save file"
   | Mark_obsolete_req _             -> fprintf fmt "mark obsolete"
   | Clean_req                       -> fprintf fmt "clean"
@@ -301,13 +300,11 @@ let print_list_loc fmt l =
 
 let print_notify fmt n =
   match n with
-  | Node_change (ni, nf)               ->
+  | Reset_whole_tree -> fprintf fmt "reset whole tree"
+  | Node_change (ni, nf) ->
       begin
         match nf with
         | Proved b -> fprintf fmt "node change %d Proved %b" ni b
-(*
-        | Obsolete b -> fprintf fmt "node change %d Obsolete %b" ni b
-*)
         | Proof_status_change(st,b,_lim) ->
            fprintf fmt "node change %d Proof_status_change res=%a obsolete=%b limits=<TODO>"
                    ni Controller_itp.print_status st b
@@ -534,6 +531,7 @@ let get_locations t =
 
 let get_modified_node n =
   match n with
+  | Reset_whole_tree -> None
   | New_node (nid, _, _, _, _) -> Some nid
   | Node_change  (nid, _) -> Some nid
   | Remove nid -> Some nid
@@ -852,30 +850,27 @@ end
   (* Initialization of session tree *)
   (**********************************)
 
+(*
   let _init_the_tree (): unit =
     let f ~parent node_id = ignore (new_node ~parent node_id) in
     iter_the_files f root_node
+*)
 
-  let init_and_send_subtree_from_trans parent trans_id : unit =
+  let send_new_subtree_from_trans parent trans_id : unit =
     iter_subtree_from_trans
       (fun ~parent id -> ignore (new_node ~parent id)) parent trans_id
 
-  let init_and_send_file f =
+  let send_new_subtree_from_file f =
     iter_subtree_from_file (fun ~parent id -> ignore (new_node ~parent id))
       root_node f
 
-  let init_and_send_the_tree (): unit =
+  let reset_and_send_the_whole_tree (): unit =
+    P.notify Reset_whole_tree;
     iter_the_files (fun ~parent id -> ignore (new_node ~parent id)) root_node
 
-  let resend_the_tree (): unit =
-    let send_node ~parent any =
-      let node_id = node_ID_from_any any in
-      let node_name = get_node_name any in
-      let node_type = get_node_type any in
-      let node_detached = get_node_detached any in
-      P.notify (New_node (node_id, parent, node_type, node_name, node_detached));
-      get_node_proved node_id any in
-    iter_the_files send_node root_node
+  let unfocus () =
+    focused_node := Unfocused;
+    reset_and_send_the_whole_tree ()
 
   (* -- send the task -- *)
   let task_of_id d id do_intros show_full_context loc =
@@ -938,7 +933,7 @@ end
             let b = add_file cont f in
             if b then
               let file = get_file cont.controller_session fn in
-              init_and_send_file file;
+              send_new_subtree_from_file file;
               read_and_send (file_name file)
           end
         else
@@ -996,7 +991,7 @@ end
     if b then
       begin
         (* Send the tree *)
-        init_and_send_the_tree ();
+        reset_and_send_the_whole_tree ();
         (* After initial sending, we don't check anymore that there is a need to
            focus on a specific node. *)
         get_focused_label := None
@@ -1084,7 +1079,7 @@ end
       let ses = d.cont.controller_session in
       let id = get_trans_parent ses trans_id in
       let nid = node_ID_from_pn id in
-      init_and_send_subtree_from_trans nid trans_id
+      send_new_subtree_from_trans nid trans_id
     | TSfailed (id, e) ->
       let doc = try
         Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
@@ -1197,11 +1192,17 @@ end
 
   let reload_session () : unit =
     let d = get_server_data () in
+    (* interrupt all running provers and unfocus before reload *)
+    C.interrupt ();
+    let _old_focus = !focused_node in
+    unfocus ();
     clear_tables ();
-    (* Calling reload_files breaks the controller if it fails *)
     let b = reload_files d.cont ~use_shapes:true in
-    if b then init_and_send_the_tree ()
-
+    if b then
+      begin
+        (* TODO: try to restore the previous focus : focused_node := old_focus; *)
+        reset_and_send_the_whole_tree ()
+      end
 
   let replay_session () : unit =
     let d = get_server_data () in
@@ -1272,33 +1273,23 @@ end
     let config = d.cont.controller_config in
     try (
     match r with
-(*
-    | Edit_req (nid, p)            ->
-      let p = try Some (get_prover p) with
-      | Bad_prover_name p -> P.notify (Message (Proof_error (nid, "Bad prover name" ^ p))); None
-      in
-      begin match p with
-      | None -> ()
-      | Some p ->
-          schedule_edition nid p
-      end
- *)
     | Clean_req                    -> clean_session ()
     | Save_req                     -> save_session ()
     | Reload_req                   -> reload_session ()
-    | Get_Session_Tree_req         -> resend_the_tree ()
     | Get_first_unproven_node ni   ->
       notify_first_unproven_node d ni
     | Focus_req nid ->
         let d = get_server_data () in
         let s = d.cont.controller_session in
         let any = any_from_node_ID nid in
-        (match any with
-        | APa pa ->
-          focused_node := Focus_on [APn (Session_itp.get_proof_attempt_parent s pa)]
-        | _ -> focused_node := Focus_on [any])
-    | Unfocus_req ->
-        focused_node := Unfocused
+        let focus_on =
+          match any with
+          | APa pa -> APn (Session_itp.get_proof_attempt_parent s pa)
+          | _ -> any
+        in
+        focused_node := Focus_on [focus_on];
+        reset_and_send_the_whole_tree ()
+    | Unfocus_req -> unfocus ()
     | Remove_subtree nid           -> remove_node nid
     | Copy_paste (from_id, to_id)    ->
         let from_any = any_from_node_ID from_id in

src/session/json_util.ml

@@ -115,6 +115,7 @@ let convert_update u =
 
 let convert_notification_constructor n =
   match n with
+  | Reset_whole_tree             -> String "Reset_whole_tree"
   | New_node _                   -> String "New_node"
   | Node_change _                -> String "Node_change"
   | Remove _                     -> String "Remove"
@@ -152,7 +153,6 @@ let convert_request_constructor (r: ide_request) =
   | Copy_paste _              -> String "Copy_paste"
   | Copy_detached _           -> String "Copy_detached"
   | Get_first_unproven_node _ -> String "Get_first_unproven_node"
-  | Get_Session_Tree_req      -> String "Get_Session_Tree_req"
   | Mark_obsolete_req _       -> String "Mark_obsolete_req"
   | Clean_req                 -> String "Clean_req"
   | Save_req                  -> String "Save_req"
@@ -202,8 +202,6 @@ let print_request_to_json (r: ide_request): Json_base.json =
                       "node_ID", Int id]
   | Unfocus_req ->
       convert_record ["ide_request", cc r]
-  | Get_Session_Tree_req ->
-      convert_record ["ide_request", cc r]
   | Mark_obsolete_req n ->
       convert_record ["ide_request", cc r;
            "node_ID", Int n]
@@ -350,6 +348,7 @@ let print_notification_to_json (n: notification): json =
   let cc = convert_notification_constructor in
   Record (
   match n with
+  | Reset_whole_tree -> convert_record ["notification", cc n]
   | New_node (nid, parent, node_type, name, detached) ->
       convert_record ["notification", cc n;
            "node_ID", Int nid;
@@ -468,10 +467,6 @@ let parse_request (constr: string) j =
   | "Copy_detached" ->
     let n = get_int (get_field j "node_ID") in
     Copy_detached n
-
-  | "Get_Session_Tree_req" ->
-    Get_Session_Tree_req
-
   | "Mark_obsolete_req" ->
     let n = get_int (get_field j "node_ID") in
     Mark_obsolete_req n

src/tools/why3shell.ml

@@ -235,6 +235,7 @@ let is_proof_attempt node_type =
 let treat_notification fmt n =
   fprintf fmt "Treat notifications@.";
   match n with
+  | Reset_whole_tree -> () (* something to do ? *)
   | Node_change (id, info)        ->
     change_node fmt id info
   | New_node (id, pid, typ, name, detached) ->