[gnome-shell] WorkspacesView: fix removal of workspaces that are not at the end

[Giovanni Campagna <gcampagna src gnome org>]

commit 1b152e6bd091cabd71ae62487e2809b392f1c540
Author: Giovanni Campagna <gcampagna src gnome org>
Date:   Fri Jan 3 19:04:06 2014 +0100

    WorkspacesView: fix removal of workspaces that are not at the end
    
    Workspaces can removed from any index, and in particular they
    will be removed by the WorkspaceTracker if they stop containing
    windows at some point. Make sure WorkspacesView is not confused
    and destroyes the right Workspace objects.
    
    https://bugzilla.gnome.org/show_bug.cgi?id=721417

 js/ui/workspacesView.js |   33 ++++++++++++++++++---------------
 1 files changed, 18 insertions(+), 15 deletions(-)
---
diff --git a/js/ui/workspacesView.js b/js/ui/workspacesView.js
index 997d1a8..1d0982b 100644
--- a/js/ui/workspacesView.js
+++ b/js/ui/workspacesView.js
@@ -237,29 +237,32 @@ const WorkspacesView = new Lang.Class({
     },
 
     _updateWorkspaces: function() {
-        let oldNumWorkspaces = this._workspaces.length;
         let newNumWorkspaces = global.screen.n_workspaces;
 
         this.scrollAdjustment.upper = newNumWorkspaces;
 
-        if (newNumWorkspaces > oldNumWorkspaces) {
-            for (let w = oldNumWorkspaces; w < newNumWorkspaces; w++) {
-                let metaWorkspace = global.screen.get_workspace_by_index(w);
-                let workspace = new Workspace.Workspace(metaWorkspace, this._monitorIndex);
-                this._workspaces.push(workspace);
+        let needsUpdate = false;
+        for (let j = 0; j < newNumWorkspaces; j++) {
+            let metaWorkspace = global.screen.get_workspace_by_index(j);
+            let workspace;
+
+            if (j >= this._workspaces.length) { /* added */
+                workspace = new Workspace.Workspace(metaWorkspace, this._monitorIndex);
                 this.actor.add_actor(workspace.actor);
+                this._workspaces[j] = workspace;
+            } else  {
+                workspace = this._workspaces[j];
+
+                if (workspace.metaWorkspace != metaWorkspace) { /* removed */
+                    workspace.destroy();
+                    this._workspaces.splice(j, 1);
+                } /* else kept */
             }
-
-            if (this._fullGeometry)
-                this._updateWorkspaceActors(false);
-        } else if (newNumWorkspaces < oldNumWorkspaces) {
-            let nRemoved = (newNumWorkspaces - oldNumWorkspaces);
-            let removed = this._workspaces.splice(oldNumWorkspaces, nRemoved);
-            removed.forEach(function(workspace) {
-                workspace.destroy();
-            });
         }
 
+        if (this._fullGeometry)
+            this._updateWorkspaceActors(false);
+
         this._syncGeometry();
     },