From d78936512b45a6ca59b8d15863dcfb9ce56fb1da Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Tue, 10 Oct 2017 14:38:57 +0200
Subject: [PATCH] IDE: split message zone into several tabs

---
 src/ide/why3ide.ml | 100 +++++++++++++++++++++++++++++++--------------
 1 file changed, 69 insertions(+), 31 deletions(-)

diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml
index fa98a7fbbf..19b034ce9d 100644
--- a/src/ide/why3ide.ml
+++ b/src/ide/why3ide.ml
@@ -869,11 +869,31 @@ let monitor =
 
 let command_entry = GEdit.entry ~packing:hbox22221#add ()
 
-(* Part 2.2.2.2.2 contains message returned by the IDE/server *)
+(* Part 2.2.2.2.2 contains messages returned by the IDE/server *)
+let messages_notebook = GPack.notebook ~packing:vbox2222#add ()
+
+let error_page,error_view =
+  let label = GMisc.label ~text:"Messages" () in
+  0, GPack.vbox ~homogeneous:false ~packing:
+    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()
+
+let log_page,log_view =
+  let label = GMisc.label ~text:"Log" () in
+  0, GPack.vbox ~homogeneous:false ~packing:
+    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()
+
 let message_zone =
   let sv = GBin.scrolled_window
       ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
-      ~shadow_type:`ETCHED_OUT ~packing:vbox2222#add ()
+      ~shadow_type:`ETCHED_OUT ~packing:error_view#add ()
+  in
+  GText.view ~editable:false ~cursor_visible:false
+    ~packing:sv#add ()
+
+let log_zone =
+  let sv = GBin.scrolled_window
+      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
+      ~shadow_type:`ETCHED_OUT ~packing:log_view#add ()
   in
   GText.view ~editable:false ~cursor_visible:false
     ~packing:sv#add ()
@@ -884,19 +904,20 @@ let message_zone_error_tag = message_zone#buffer#create_tag
 
 (**** Message-zone printing functions *****)
 
+let add_to_log mark s =
+  log_zone#buffer#insert ("\n--------["^ mark ^"]--------\n");
+  log_zone#buffer#insert s;
+  log_zone#scroll_to_mark `INSERT
+
 (* Function used to print stuff on the message_zone *)
-let print_message fmt =
+let print_message ~kind ~mark fmt =
   Format.kfprintf
     (fun _ -> let s = flush_str_formatter () in
-              message_zone#buffer#set_text s)
+              add_to_log mark s;
+              if kind>0 then message_zone#buffer#set_text s)
     str_formatter
     fmt
 
-(*let add_to_msg_zone s =
-  let s = message_zone#buffer#get_text () ^ "\n" ^ s in
-  message_zone#buffer#set_text s;
-  message_zone#scroll_to_mark `INSERT
- *)
 
 (**** Monitor *****)
 
@@ -1319,16 +1340,19 @@ let (_ : GtkSignal.id) =
 
 let treat_message_notification msg = match msg with
   (* TODO: do something ! *)
-  | Proof_error (_id, s)                        -> print_message "Proof_error: %s" s
+  | Proof_error (_id, s)                        ->
+     print_message ~kind:1 ~mark:"[Proof_error]" "%s" s
   | Transf_error (_id, tr_name, arg, loc, msg, doc) ->
       if arg = "" then
-        print_message "%s\nTransformation failed: \n%s\n\n%s" msg tr_name doc
+        print_message ~kind:1 ~mark:"Transformation Error"
+                      "%s\nTransformation failed: \n%s\n\n%s" msg tr_name doc
       else
         begin
           let buf = message_zone#buffer in
           (* remove all coloration in message_zone *)
           buf#remove_tag_by_name "error" ~start:buf#start_iter ~stop:buf#end_iter;
-          print_message "%s\nTransformation failed. \nOn argument: \n%s \n%s\n\n%s"
+          print_message ~kind:1 ~mark:"Transformation Error"
+                        "%s\nTransformation failed. \nOn argument: \n%s \n%s\n\n%s"
             tr_name arg msg doc;
           let color = "error" in
           let _, _, beg_char, end_char = Loc.get loc in
@@ -1338,19 +1362,26 @@ let treat_message_notification msg = match msg with
             ~stop:(start#forward_chars end_char)
             color
         end
-  | Strat_error (_id, s)                        -> print_message "Strat_error: %s" s
-  | Replay_Info s                               -> print_message "Replay_info: %s" s
-  | Query_Info (_id, s)                         -> print_message "Query_info: %s" s
-  | Query_Error (_id, s)                        -> print_message "Query_error: %s" s
-  | Help s                                      -> print_message "Help: %s" s
-  | Information s                               -> print_message "Information: %s" s
-  | Task_Monitor (t, s, r)                      -> update_monitor t s r
-  | Open_File_Error s                           -> print_message "Open_File_Error: %s" s
-  | Parse_Or_Type_Error (loc, s)                ->
+  | Strat_error (_id, s) ->
+     print_message ~kind:1 ~mark:"Strat_error" "%s" s
+  | Replay_Info s ->
+     print_message ~kind:0 ~mark:"Replay_info" "%s" s
+  | Query_Info (_id, s) ->
+     print_message ~kind:1 ~mark:"Query_info" "%s" s
+  | Query_Error (_id, s) ->
+     print_message ~kind:1 ~mark:"Query_error" "%s" s
+  | Help s ->
+     print_message ~kind:1 ~mark:"Help" "%s" s
+  | Information s ->
+     print_message ~kind:1 ~mark:"Information" "%s" s
+  | Task_Monitor (t, s, r) -> update_monitor t s r
+  | Open_File_Error s ->
+     print_message ~kind:0 ~mark:"Open_File_Error" "%s" s
+  | Parse_Or_Type_Error (loc, s) ->
     begin
       (* TODO find a new color *)
       color_loc ~color:Goal_color loc;
-      print_message "Parse_Or_Type_Error: %s" s
+      print_message ~kind:1 ~mark:"Parse_Or_Type_Error]" "%s" s
     end
   | File_Saved f                 ->
     begin
@@ -1358,13 +1389,14 @@ let treat_message_notification msg = match msg with
         let (_source_page, _source_view, b, l) = Hstr.find source_view_table f in
         b := false;
         update_label_saved l;
-        print_message "%s was saved" f
+        print_message ~kind:1 ~mark:"File_Saved" "%s was saved" f
       with
       | Not_found                ->
-          print_message "Please report: %s was not found in IDE but was saved in session" f
+          print_message ~kind:1 ~mark:"File_Saved"
+                        "Please report: %s was not found in IDE but was saved in session" f
     end
   | Error s                      ->
-     print_message "Request failed: %s" s
+     print_message ~kind:1 ~mark:"General request failure" "%s" s
 
 
 (***********************)
@@ -1733,7 +1765,8 @@ let () =
                | [r] ->
                    let id = get_node_id r#iter in
                    send_request (Remove_subtree id)
-               | _ -> print_message "Select only one node to perform this action");
+               | _ -> print_message ~kind:1 ~mark:"Remove_subtree error"
+                        "Select only one node to perform the remove node action");
   connect_menu_item
     edit_menu_item
     ~callback:(fun () ->
@@ -1741,7 +1774,8 @@ let () =
                | [r] ->
                    let id = get_node_id r#iter in
                    send_request (Command_req (id,"edit"))
-               | _ -> print_message "Select only one node to perform this action");
+               | _ -> print_message ~kind:1 ~mark:"Edit error"
+                        "Select only one node to perform the edit action");
   connect_menu_item
     mark_obsolete_item
     ~callback:(fun () ->
@@ -1749,7 +1783,8 @@ let () =
                | [r] ->
                    let id = get_node_id r#iter in
                    send_request (Mark_obsolete_req id)
-               | _ -> print_message "Select only one node to perform this action");
+               | _ -> print_message ~kind:1 ~mark:"Mark_obsolete error"
+                        "Select only one node to perform the mark obsolete action");
   connect_menu_item
     focus_item
     ~callback:(fun () ->
@@ -1760,7 +1795,8 @@ let () =
           (* TODO not efficient *)
           clear_tree_and_table goals_model;
           send_request (Get_Session_Tree_req);
-      | _ -> print_message "Select only one node to perform this action");
+      | _ -> print_message ~kind:1 ~mark:"Focus_req error"
+                        "Select only one node to perform the focus action");
   connect_menu_item
     unfocus_item
     ~callback:(fun () ->
@@ -1844,7 +1880,8 @@ let treat_notification n =
      init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
   | Saved                         ->
       session_needs_saving := false;
-      print_message "Session saved.";
+      print_message ~kind:1 ~mark:"Saved action info"
+                        "Session saved.";
       if !quit_on_saved = true then
         exit_function_safe ()
   | Message (msg)                 -> treat_message_notification msg
@@ -1866,7 +1903,8 @@ let treat_notification n =
       | Not_found -> create_source_view file_name content
     end
   | Dead _ ->
-     print_message "Serveur sent an unexpected notification '%a'. Please report."
+     print_message ~kind:1 ~mark:"Server Dead ?"
+                        "Server sent the notification '%a'. Please report."
         print_notify n
   end;
   ()
-- 
GitLab