Update TUI window title when changed

I wrote a TUI window in Python, and I noticed that setting its title
did not result in a refresh, so the new title did not appear.  This
patch corrects this problem.

2 files changed, 15 insertions, 0 deletions

diff --git a/gdb/tui/tui-data.c b/gdb/tui/tui-data.c
index 0daed32..abd2ec2 100644
--- a/gdb/tui/tui-data.c
+++ b/gdb/tui/tui-data.c
@@ -152,6 +152,17 @@ tui_prev_win (struct tui_win_info *cur_win)
   return *iter;
 }
 
+/* See tui-data.h.  */
+
+void
+tui_win_info::set_title (const char *new_title)
+{
+  if (title != new_title)
+    {
+      title = new_title;
+      check_and_display_highlight_if_needed ();
+    }
+}
 
 void
 tui_win_info::rerender ()
diff --git a/gdb/tui/tui-data.h b/gdb/tui/tui-data.h
index c92e85c..030ce2a 100644
--- a/gdb/tui/tui-data.h
+++ b/gdb/tui/tui-data.h
@@ -146,6 +146,10 @@ public:
 
   void check_and_display_highlight_if_needed ();
 
+  /* A helper function to change the title and then redraw the
+     surrounding box, if needed.  */
+  void set_title (const char *new_title);
+
   /* Window handle.  */
   std::unique_ptr<WINDOW, curses_deleter> handle;
   /* Window width.  */