window-list: add a workspace switcher

This is the most basic version of a workspace switcher, taken from
Frippery Bottom Panel and adapted. It handles clicks and scrolls,
and does not show window thumbnails or shapes.
Note that, differently from the frippery version, it won't change
the workspace layout, and actually assume a linear vertical layout,
which is then shown horizontally. This is to keep compatibility
with the overview, which uses a vertical layout.

https://bugzilla.gnome.org/show_bug.cgi?id=694914

extensions/window-list/extension.js

@@ -401,6 +401,9 @@ const WindowList = new Lang.Class({
                 this._windowList.layout_manager.spacing = spacing;
             }));
 
+        this._workspaceSwitcher = new WorkspaceSwitcher();
+        box.add(this._workspaceSwitcher.actor);
+
         this._trayButton = new TrayButton();
         box.add(this._trayButton.actor);
 
@@ -684,6 +687,137 @@ const WindowList = new Lang.Class({
     }
 });
 
+// Some of this class and the following one were
+// copied from Frippery Bottom Panel
+// Copyright 2011-2012 R M Yorston
+
+const WorkspaceButton = new Lang.Class({
+    Name: 'WorkspaceButton',
+
+    _init: function(index) {
+        this.actor = new St.Button({ name: 'workspaceButton',
+                                     style_class: 'window-list-workspace-button',
+                                     reactive: true });
+        this.actor.connect('clicked', Lang.bind(this, this._onClicked));
+
+        this.label = new St.Label();
+        this.actor.set_child(this.label);
+
+        this.actor.label_actor = this.label;
+        this.setIndex(index);
+    },
+
+    _onClicked: function() {
+	if (this.index >= 0 && this.index < global.screen.n_workspaces) {
+            let metaWorkspace = global.screen.get_workspace_by_index(this.index);
+	    metaWorkspace.activate(global.get_current_time());
+        }
+
+        return true;
+    },
+
+    setIndex: function(index) {
+        if (index < 0 || index >= global.screen.n_workspaces) {
+            return;
+        }
+
+        this.index = index;
+
+        let active = global.screen.get_active_workspace_index();
+        this.setActive(index == active);
+    },
+
+    setActive: function(active) {
+        if (active) {
+	    this.label.set_text('-' + (this.index + 1) + '-');
+	    this.actor.add_style_pseudo_class('outlined');
+        } else {
+            this.label.set_text(String(this.index + 1));
+            this.actor.remove_style_pseudo_class('outlined');
+        }
+    }
+});
+
+const WorkspaceSwitcher = new Lang.Class({
+    Name: 'WorkspaceSwitcher',
+
+    _init: function() {
+        this.actor = new St.BoxLayout({ name: 'workspaceSwitcher',
+                                        style_class: 'window-list-workspace-switcher',
+                                        reactive: true });
+	this.actor.connect('scroll-event', this._onScroll);
+        this.actor.connect('destroy', this._onDestroy);
+        this.actor._delegate = this;
+        this.button = [];
+        this._active = 0;
+        this._createButtons();
+
+        this._nWorkspacesId = global.screen.connect('notify::n-workspaces',
+                                                    Lang.bind(this, this._createButtons));
+	this._switchWorkspaceId = global.screen.connect('workspace-switched',
+	                                                Lang.bind(this, this._updateButtons));
+    },
+
+    _onDestroy: function() {
+        if (this._nWorkspacesId) {
+            global.screen.disconnect(this._nWorkspacesId);
+            this._nWorkspacesId = 0;
+        }
+
+        if (this._switchWorkspaceId) {
+            global.screen.disconnect(this._switchWorkspaceId);
+            this._switchWorkspaceId = 0;
+        }
+    },
+
+    _createButtons: function() {
+        let nPresent = this.actor.get_n_children();
+        let nWanted = global.screen.n_workspaces;
+        if (nPresent == nWanted)
+            return;
+
+        if (nPresent > nWanted) {
+            for (let i = nWanted; i < nPresent; i++)
+                this.button[i].actor.destroy();
+        } else {
+            for (let i = nPresent; i < nWanted; i++) {
+                let button = new WorkspaceButton(i);
+                this.button[i] = button;
+                this.actor.insert_child_at_index(button.actor, i);
+            }
+        }
+
+        this.button.length = nWanted;
+    },
+
+    _updateButtons: function() {
+        let active = global.screen.get_active_workspace_index();
+        this.button[this._active].setActive(false);
+        this.button[active].setActive(true);
+
+        this._active = active;
+    },
+
+    _onScroll: function(actor, event) {
+        let direction = event.get_scroll_direction();
+
+        let metaDirection;
+        if (direction == Clutter.ScrollDirection.UP)
+            metaDirection = Meta.MotionDirection.UP;
+        else if (direction == Clutter.ScrollDirection.DOWN)
+            metaDirection = Meta.MotionDirection.DOWN;
+        else
+            // We don't handle any other direction
+            return;
+
+        let activeWorkspace = global.screen.get_active_workspace();
+        let toActivate = activeWorkspace.get_neighbor(metaDirection);
+
+        if (activeWorkspace != toActivate)
+            toActivate.activate(global.get_current_time());
+    },
+});
+
 let windowList;
 let injections = {};
 let notificationParent;

extensions/window-list/stylesheet.css

@@ -1,8 +1,5 @@
 .bottom-panel {
-  /* .window-button-icon height +
-     .window-button vertical padding +
-     .window-button > StWidget vertical padding) */
-  height: 30px;
+  height: 32px;
 }
 
 .window-list {
@@ -65,3 +62,28 @@
   width: 24px;
   height: 24px;
 }
+
+.window-list-workspace-switcher {
+  spacing: 6px;
+}
+
+.window-list-workspace-button {
+  min-width: 2.5em;
+  color: #ccc;
+  transition-duration: 100;
+  border: 1px;
+  border-color: #ccc;
+  padding: 0 2px;
+}
+
+.window-list-workspace-button:outlined {
+  padding: 0 1px;
+  border: 2px solid white;
+  background: #222;
+  font-weight: bold;
+}
+
+.window-list-workspace-button:hover {
+  color: white;
+  text-shadow: black 0px 2px 2px;
+}