diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml index 75eae35c98884c7a61bb3a905dce228c130ad396..4300c26946da23652ce9aa03bcf087a8455bfb69 100644 --- a/src/ide/why3ide.ml +++ b/src/ide/why3ide.ml @@ -454,8 +454,10 @@ let message_zone = (**** Message-zone printing functions *****) (* Function used to print stuff on the message_zone *) -let print_message s = - message_zone#buffer#set_text s +let print_message fmt = + Format.kasprintf + message_zone#buffer#set_text + fmt let add_to_msg_zone s = let s = message_zone#buffer#get_text () ^ "\n" ^ s in @@ -878,21 +880,21 @@ let open_session: GMenu.menu_item = let treat_message_notification msg = match msg with (* TODO: do something ! *) - | Proof_error (_id, s) -> print_message s - | Transf_error (_id, s) -> print_message s - | Strat_error (_id, s) -> print_message s - | Replay_Info s -> print_message s - | Query_Info (_id, s) -> print_message s - | Query_Error (_id, s) -> print_message s - | Help s -> print_message s - | Information s -> print_message s + | Proof_error (_id, s) -> print_message "%s" s + | Transf_error (_id, s) -> print_message "%s" s + | Strat_error (_id, s) -> print_message "%s" s + | Replay_Info s -> print_message "%s" s + | Query_Info (_id, s) -> print_message "%s" s + | Query_Error (_id, s) -> print_message "%s" s + | Help s -> print_message "%s" s + | Information s -> print_message "%s" s | Task_Monitor (t, s, r) -> update_monitor t s r - | Open_File_Error s -> print_message s + | Open_File_Error s -> print_message "%s" s | Error s -> if Debug.test_flag debug then - print_message s + print_message "%s" s else - print_message "Request failed." + print_message "%s" "Request failed. You can get details using --debug ide_info" (***********************) @@ -968,17 +970,18 @@ let treat_notification n = match n with | Initialized g_info -> (* TODO: treat other *) init_completion g_info.provers g_info.transformations g_info.commands; - | Saved -> (* TODO *) - print_message "got a Saved notification not yet supported\n" + | Saved -> + print_message "Session saved." | Message (msg) -> treat_message_notification msg - | Dead _s -> (* TODO *) - print_message "got a Dead notification not yet supported\n" | Task (_id, s) -> (* TODO: check that the id is the current one *) task_view#source_buffer#set_text s; (* scroll to end of text *) task_view#scroll_to_mark `INSERT - | File_contents _ -> assert false (* This IDE never requests file contents *) + | File_contents _ + | Dead _ -> + print_message "Serveur sent an unexpected notification '%a'. Please report." print_notify n + (***********************) (* start the interface *) diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index a568076d8f24cb56ca67ca39a23344bb29a090b5..73118a3c520fc6ce035f2ad7f45ca8e1ffb92f20 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -688,7 +688,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct init_and_send_file file end else - P.notify (Message (Open_File_Error ("Not a file: " ^ f))) + P.notify (Message (Open_File_Error ("File not found: " ^ f))) else P.notify (Message (Open_File_Error ("File already in session: " ^ fn))) @@ -737,7 +737,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct end else begin - P.notify (Message (Open_File_Error ("Not a file: " ^ f))); + P.notify (Message (Open_File_Error ("File not found: " ^ f))); false end) with