fix #146 Unfocus_req does not need a node to be selected

Also, better errors when no node is selected.

src/ide/why3ide.ml

@@ -2160,9 +2160,7 @@ let (_ : GMenu.menu_item) =
     ~callback
 
 let (_ : GMenu.menu_item) =
-  let callback =
-    on_selected_rows ~multiple:false ~notif_kind:"Unfocus_req error" ~action:"unfocus"
-      (fun id -> Command_req (id, "Unfocus")) in
+  let callback = fun () -> send_request (Unfocus_req) in
   tools_factory#add_item "_Unfocus"
     ~callback
 

src/session/itp_communication.ml

@@ -115,6 +115,7 @@ type ide_request =
   | Copy_paste              of node_ID * node_ID
   | Save_file_req           of string * string
   | Get_first_unproven_node of node_ID
+  | Unfocus_req
   | Save_req
   | Reload_req
   | Exit_req
@@ -129,7 +130,7 @@ let modify_session (r: ide_request) =
 
   | Set_config_param _ | Set_prover_policy _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _
-  | Save_req | Exit_req | Get_global_infos
+  | Unfocus_req | Save_req | Exit_req | Get_global_infos
   | Interrupt_req -> false
 
 
@@ -147,10 +148,11 @@ let print_request fmt r =
              Whyconf.print_prover_upgrade_policy p2
   | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
-  | Get_task(nid,b,loc)           -> fprintf fmt "get task(%d,%b,%b)" nid b loc
+  | Get_task(nid,b,loc)             -> fprintf fmt "get task(%d,%b,%b)" nid b loc
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
   | Copy_paste _                    -> fprintf fmt "copy paste"
   | Save_file_req _                 -> fprintf fmt "save file"
+  | Unfocus_req                     -> fprintf fmt "unfocus"
   | Save_req                        -> fprintf fmt "save"
   | Reload_req                      -> fprintf fmt "reload"
   | Exit_req                        -> fprintf fmt "exit"

src/session/itp_communication.mli

@@ -133,6 +133,7 @@ type ide_request =
   | Save_file_req           of string * string
   (** [Save_file_req(filename, content_of_file)] saves the file *)
   | Get_first_unproven_node of node_ID
+  | Unfocus_req
   | Save_req
   | Reload_req
   | Exit_req

src/session/itp_server.ml

@@ -1304,7 +1304,7 @@ end
      match r with
      | Save_req | Reload_req | Get_file_contents _ | Save_file_req _
      | Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
-     | Exit_req | Get_global_infos -> true
+     | Exit_req | Get_global_infos | Itp_communication.Unfocus_req -> true
      | Get_first_unproven_node ni ->
          Hint.mem model_any ni
      | Remove_subtree nid ->
@@ -1396,7 +1396,7 @@ end
             in
             focused_node := Focus_on [focus_on];
             reset_and_send_the_whole_tree ()
-        | Unfocus_req -> unfocus ()
+        | Server_utils.Unfocus_req -> unfocus ()
         | Help_message s          -> P.notify (Message (Information s))
         | QError s                -> P.notify (Message (Query_Error (nid, s)))
         | Other (s, _args)        ->
@@ -1427,6 +1427,7 @@ end
     | Set_prover_policy(p,u)   ->
        let c = d.cont in
        Controller_itp.set_session_prover_upgrade_policy c p u
+    | Unfocus_req             -> unfocus ()
     | Exit_req                -> exit 0
      )
     with

src/session/json_util.ml

@@ -164,6 +164,7 @@ let convert_request_constructor (r: ide_request) =
   | Remove_subtree _          -> String "Remove_subtree"
   | Copy_paste _              -> String "Copy_paste"
   | Get_first_unproven_node _ -> String "Get_first_unproven_node"
+  | Unfocus_req               -> String "Unfocus_req"
   | Save_req                  -> String "Save_req"
   | Reload_req                -> String "Reload_req"
   | Exit_req                  -> String "Exit_req"
@@ -216,6 +217,7 @@ let print_request_to_json (r: ide_request): Json_base.json =
   | Get_first_unproven_node id ->
       convert_record ["ide_request", cc r;
            "node_ID", Int id]
+  | Unfocus_req
   | Save_req
   | Reload_req
   | Exit_req
@@ -482,6 +484,10 @@ let parse_request (constr: string) j =
     let to_id = get_int (get_field j "node_ID2") in
     Copy_paste (from_id, to_id)
 
+  | "Unfocus_req" ->
+    Unfocus_req
+  | "Interrupt_req" ->
+    Interrupt_req
   | "Save_req" ->
     Save_req
   | "Reload_req" ->

src/session/server_utils.ml

@@ -409,7 +409,9 @@ let interp commands_table cont id s =
               QError (Format.asprintf "Prover %a was recognized but arguments were not parsed" Whyconf.print_prover prover)
           | Not_Prover ->
              if Hstr.mem cont.Controller_itp.controller_strategies cmd then
-               Strategies cmd
+               match id with
+               | None   -> QError ("Please select a node in the task tree")
+               | Some _ -> Strategies cmd
              else
                match cmd, args with
                | "edit", _ ->
@@ -438,7 +440,12 @@ let interp commands_table cont id s =
                | "mark", _ ->
                    Mark_Obsolete
                | "Focus", _ ->
-                   Focus_req
+                   begin
+                     match id with
+                     | None ->
+                         QError ("Select at least one node of the task tree")
+                     | Some _ -> Focus_req
+                   end
                | "Unfocus", _ ->
                    Unfocus_req
                | "clean", _ ->