[gnome-shell-extensions] workspace-indicator: Support horizontal workspace layout

[Florian Müllner <fmuellner src gnome org>]

commit 52f373fb70163e564726cf0ca0d0d3b95195562d
Author: Florian Müllner <fmuellner gnome org>
Date:   Sun Jun 9 23:45:24 2019 +0000

    workspace-indicator: Support horizontal workspace layout
    
    Just like we did for the workspace indicator in the window-list, improve
    the handling of horizontal workspace layouts by showing the switcher
    in-place instead of delegating the functionality to a menu.
    
    https://gitlab.gnome.org/GNOME/gnome-shell-extensions/merge_requests/71

 extensions/workspace-indicator/extension.js   | 75 ++++++++++++++++++++++++++-
 extensions/workspace-indicator/stylesheet.css | 27 +++++++++-
 2 files changed, 99 insertions(+), 3 deletions(-)
---
diff --git a/extensions/workspace-indicator/extension.js b/extensions/workspace-indicator/extension.js
index 82700b0..3e6e939 100644
--- a/extensions/workspace-indicator/extension.js
+++ b/extensions/workspace-indicator/extension.js
@@ -14,11 +14,37 @@ const _ = Gettext.gettext;
 const WORKSPACE_SCHEMA = 'org.gnome.desktop.wm.preferences';
 const WORKSPACE_KEY = 'workspace-names';
 
+let WorkspaceThumbnail = GObject.registerClass({
+    GTypeName: 'WorkspaceIndicatorWorkspaceThumbnail'
+}, class WorkspaceThumbnail extends St.Button {
+    _init(index) {
+        super._init({
+            style_class: 'workspace',
+        });
+
+        this._index = index;
+    }
+
+    on_clicked() {
+        let ws = global.workspace_manager.get_workspace_by_index(this._index);
+        if (ws)
+            ws.activate(global.get_current_time());
+    }
+});
+
+
 let WorkspaceIndicator = GObject.registerClass(
 class WorkspaceIndicator extends PanelMenu.Button {
     _init() {
         super._init(0.0, _('Workspace Indicator'));
 
+        let container = new St.Widget({
+            layout_manager: new Clutter.BinLayout(),
+            x_expand: true,
+            y_expand: true
+        });
+        this.add_actor(container);
+
         let workspaceManager = global.workspace_manager;
 
         this._currentWorkspace = workspaceManager.get_active_workspace_index();
@@ -28,7 +54,15 @@ class WorkspaceIndicator extends PanelMenu.Button {
             text: this._labelText()
         });
 
-        this.add_actor(this._statusLabel);
+        container.add_actor(this._statusLabel);
+
+        this._thumbnailsBox = new St.BoxLayout({
+            style_class: 'panel-workspace-indicator-box',
+            y_expand: true,
+            reactive: true
+        });
+
+        container.add_actor(this._thumbnailsBox);
 
         this._workspacesItems = [];
         this._workspaceSection = new PopupMenu.PopupMenuSection();
@@ -38,11 +72,16 @@ class WorkspaceIndicator extends PanelMenu.Button {
             workspaceManager.connect_after('notify::n-workspaces',
                 this._nWorkspacesChanged.bind(this)),
             workspaceManager.connect_after('workspace-switched',
-                this._onWorkspaceSwitched.bind(this))
+                this._onWorkspaceSwitched.bind(this)),
+            workspaceManager.connect('notify::layout-rows',
+                this._onWorkspaceOrientationChanged.bind(this))
         ];
 
         this.connect('scroll-event', this._onScrollEvent.bind(this));
+        this._thumbnailsBox.connect('scroll-event', this._onScrollEvent.bind(this));
         this._createWorkspacesSection();
+        this._updateThumbnails();
+        this._onWorkspaceOrientationChanged();
 
         this._settings = new Gio.Settings({ schema_id: WORKSPACE_SCHEMA });
         this._settingsChangedId = this._settings.connect(
@@ -62,16 +101,26 @@ class WorkspaceIndicator extends PanelMenu.Button {
         super._onDestroy();
     }
 
+    _onWorkspaceOrientationChanged() {
+        let vertical = global.workspace_manager.layout_rows == -1;
+        this.reactive = vertical;
+
+        this._statusLabel.visible = vertical;
+        this._thumbnailsBox.visible = !vertical;
+    }
+
     _onWorkspaceSwitched() {
         this._currentWorkspace = global.workspace_manager.get_active_workspace_index();
 
         this._updateMenuOrnament();
+        this._updateActiveThumbnail();
 
         this._statusLabel.set_text(this._labelText());
     }
 
     _nWorkspacesChanged() {
         this._createWorkspacesSection();
+        this._updateThumbnails();
     }
 
     _updateMenuOrnament() {
@@ -82,6 +131,16 @@ class WorkspaceIndicator extends PanelMenu.Button {
         }
     }
 
+    _updateActiveThumbnail() {
+        let thumbs = this._thumbnailsBox.get_children();
+        for (let i = 0; i < thumbs.length; i++) {
+            if (i == this._currentWorkspace)
+                thumbs[i].add_style_class_name('active');
+            else
+                thumbs[i].remove_style_class_name('active');
+        }
+    }
+
     _labelText(workspaceIndex) {
         if (workspaceIndex == undefined) {
             workspaceIndex = this._currentWorkspace;
@@ -119,6 +178,18 @@ class WorkspaceIndicator extends PanelMenu.Button {
         this._statusLabel.set_text(this._labelText());
     }
 
+    _updateThumbnails() {
+        let workspaceManager = global.workspace_manager;
+
+        this._thumbnailsBox.destroy_all_children();
+
+        for (let i = 0; i < workspaceManager.n_workspaces; i++) {
+            let thumb = new WorkspaceThumbnail(i);
+            this._thumbnailsBox.add_actor(thumb);
+        }
+        this._updateActiveThumbnail();
+    }
+
     _activate(index) {
         let workspaceManager = global.workspace_manager;
 
diff --git a/extensions/workspace-indicator/stylesheet.css b/extensions/workspace-indicator/stylesheet.css
index 1271f1c..5118194 100644
--- a/extensions/workspace-indicator/stylesheet.css
+++ b/extensions/workspace-indicator/stylesheet.css
@@ -1,5 +1,30 @@
 .panel-workspace-indicator {
        padding: 0 8px;
-       background-color: rgba(200, 200, 200, .5);
+}
+
+.panel-workspace-indicator-box {
+       padding: 2px 0;
+}
+
+.panel-workspace-indicator-box .workspace {
+       width: 40px;
+}
+
+.panel-workspace-indicator,
+.panel-workspace-indicator-box .workspace {
        border: 1px solid #cccccc;
 }
+
+.panel-workspace-indicator,
+.panel-workspace-indicator-box .workspace.active {
+       background-color: rgba(200, 200, 200, .5);
+}
+
+.panel-workspace-indicator-box .workspace {
+    background-color: rgba(200, 200, 200, .3);
+    border-left-width: 0;
+}
+
+.panel-workspace-indicator-box .workspace:first-child {
+    border-left-width: 1px;
+}