[gnome-shell-extensions/wip/rstrode/heads-up-display: 39/62] workspace-indicator: Update workspace names in-place

[Ray Strode <halfline src gnome org>]

commit 9480ed155f2d5b2d61c2e7c241db54dc2f71b7c8
Author: Florian Müllner <fmuellner gnome org>
Date:   Sun Jun 9 23:03:55 2019 +0000

    workspace-indicator: Update workspace names in-place
    
    There's no good reason to rebuild the entire menu on workspace names
    changes, we can simply update the labels in-place.
    
    https://gitlab.gnome.org/GNOME/gnome-shell-extensions/merge_requests/71

 extensions/workspace-indicator/extension.js | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)
---
diff --git a/extensions/workspace-indicator/extension.js b/extensions/workspace-indicator/extension.js
index e052181..205ee36 100644
--- a/extensions/workspace-indicator/extension.js
+++ b/extensions/workspace-indicator/extension.js
@@ -49,9 +49,9 @@ class WorkspaceIndicator extends PanelMenu.Button {
         this._statusLabel.add_style_class_name('panel-workspace-indicator');
 
         this._settings = new Gio.Settings({ schema_id: WORKSPACE_SCHEMA });
-        this._settingsChangedId =
-            this._settings.connect(`changed::${WORKSPACE_KEY}`,
-                                   this._createWorkspacesSection.bind(this));
+        this._settingsChangedId = this._settings.connect(
+            `changed::${WORKSPACE_KEY}`,
+            this._updateMenuLabels.bind(this));
     }
 
     _onDestroy() {
@@ -82,6 +82,11 @@ class WorkspaceIndicator extends PanelMenu.Button {
         return Meta.prefs_get_workspace_name(workspaceIndex);
     }
 
+    _updateMenuLabels() {
+        for (let i = 0; i < this._workspacesItems.length; i++)
+            this._workspacesItems[i].label.text = this._labelText(i);
+    }
+
     _createWorkspacesSection() {
         let workspaceManager = global.workspace_manager;