|
|
e8fd09 |
From 8cb224b951f7271bcc73ae96a5d397ddc888a49c Mon Sep 17 00:00:00 2001
|
|
|
e8fd09 |
From: Felipe Borges <felipeborges@gnome.org>
|
|
|
e8fd09 |
Date: Fri, 20 Jan 2017 15:10:11 +0100
|
|
|
e8fd09 |
Subject: [PATCH] window-list: Hide workspace indicator when there's 1
|
|
|
e8fd09 |
workspace
|
|
|
e8fd09 |
|
|
|
e8fd09 |
There's no need to show the workspace indicator at the right
|
|
|
e8fd09 |
corner of the window-list if there's just a single workspace
|
|
|
e8fd09 |
AND the workspace creation is static. This saves us a bit more
|
|
|
e8fd09 |
of space.
|
|
|
e8fd09 |
|
|
|
e8fd09 |
https://bugzilla.gnome.org/show_bug.cgi?id=777504
|
|
|
e8fd09 |
---
|
|
|
e8fd09 |
extensions/window-list/extension.js | 25 +++++++++++++++++++++----
|
|
|
e8fd09 |
1 file changed, 21 insertions(+), 4 deletions(-)
|
|
|
e8fd09 |
|
|
|
e8fd09 |
diff --git a/extensions/window-list/extension.js b/extensions/window-list/extension.js
|
|
|
e8fd09 |
index 15db297..4d1f83c 100644
|
|
|
e8fd09 |
--- a/extensions/window-list/extension.js
|
|
|
e8fd09 |
+++ b/extensions/window-list/extension.js
|
|
|
e8fd09 |
@@ -813,10 +813,15 @@ const WindowList = new Lang.Class({
|
|
|
e8fd09 |
this._workspaceIndicator = new WorkspaceIndicator();
|
|
|
e8fd09 |
indicatorsBox.add(this._workspaceIndicator.container, { expand: false, y_fill: true });
|
|
|
e8fd09 |
|
|
|
e8fd09 |
+ this._mutterSettings = new Gio.Settings({ schema_id: 'org.gnome.mutter' });
|
|
|
e8fd09 |
this._workspaceSettings = this._getWorkspaceSettings();
|
|
|
e8fd09 |
this._workspacesOnlyOnPrimaryChangedId =
|
|
|
e8fd09 |
this._workspaceSettings.connect('changed::workspaces-only-on-primary',
|
|
|
e8fd09 |
Lang.bind(this, this._updateWorkspaceIndicatorVisibility));
|
|
|
e8fd09 |
+ this._dynamicWorkspacesSettings = this._getDynamicWorkspacesSettings();
|
|
|
e8fd09 |
+ this._dynamicWorkspacesChangedId =
|
|
|
e8fd09 |
+ this._dynamicWorkspacesSettings.connect('changed::dynamic-workspaces',
|
|
|
e8fd09 |
+ Lang.bind(this, this._updateWorkspaceIndicatorVisibility));
|
|
|
e8fd09 |
this._updateWorkspaceIndicatorVisibility();
|
|
|
e8fd09 |
|
|
|
e8fd09 |
this._menuManager = new PopupMenu.PopupMenuManager(this);
|
|
|
e8fd09 |
@@ -898,11 +903,17 @@ const WindowList = new Lang.Class({
|
|
|
e8fd09 |
this._groupingModeChanged();
|
|
|
e8fd09 |
},
|
|
|
e8fd09 |
|
|
|
e8fd09 |
+ _getDynamicWorkspacesSettings: function() {
|
|
|
e8fd09 |
+ if (this._workspaceSettings.list_keys().indexOf('dynamic-workspaces') > -1)
|
|
|
e8fd09 |
+ return this._workspaceSettings;
|
|
|
e8fd09 |
+ return this._mutterSettings;
|
|
|
e8fd09 |
+ },
|
|
|
e8fd09 |
+
|
|
|
e8fd09 |
_getWorkspaceSettings: function() {
|
|
|
e8fd09 |
let settings = global.get_overrides_settings();
|
|
|
e8fd09 |
if (settings.list_keys().indexOf('workspaces-only-on-primary') > -1)
|
|
|
e8fd09 |
return settings;
|
|
|
e8fd09 |
- return new Gio.Settings({ schema_id: 'org.gnome.mutter' });
|
|
|
e8fd09 |
+ return this._mutterSettings;
|
|
|
e8fd09 |
},
|
|
|
e8fd09 |
|
|
|
e8fd09 |
_onScrollEvent: function(actor, event) {
|
|
|
e8fd09 |
@@ -936,9 +947,12 @@ const WindowList = new Lang.Class({
|
|
|
e8fd09 |
},
|
|
|
e8fd09 |
|
|
|
e8fd09 |
_updateWorkspaceIndicatorVisibility: function() {
|
|
|
e8fd09 |
- this._workspaceIndicator.actor.visible =
|
|
|
e8fd09 |
- this._monitor == Main.layoutManager.primaryMonitor ||
|
|
|
e8fd09 |
- !this._workspaceSettings.get_boolean('workspaces-only-on-primary');
|
|
|
e8fd09 |
+ let hasWorkspaces = this._dynamicWorkspacesSettings.get_boolean('dynamic-workspaces') ||
|
|
|
e8fd09 |
+ global.screen.n_workspaces > 1;
|
|
|
e8fd09 |
+ let workspacesOnMonitor = this._monitor == Main.layoutManager.primaryMonitor ||
|
|
|
e8fd09 |
+ !this._workspaceSettings.get_boolean('workspaces-only-on-primary');
|
|
|
e8fd09 |
+
|
|
|
e8fd09 |
+ this._workspaceIndicator.actor.visible = hasWorkspaces && workspacesOnMonitor;
|
|
|
e8fd09 |
},
|
|
|
e8fd09 |
|
|
|
e8fd09 |
_getPreferredUngroupedWindowListWidth: function() {
|
|
|
e8fd09 |
@@ -1109,6 +1123,8 @@ const WindowList = new Lang.Class({
|
|
|
e8fd09 |
Lang.bind(this, this._onWindowRemoved));
|
|
|
e8fd09 |
this._workspaceSignals.set(workspace, signals);
|
|
|
e8fd09 |
}
|
|
|
e8fd09 |
+
|
|
|
e8fd09 |
+ this._updateWorkspaceIndicatorVisibility();
|
|
|
e8fd09 |
},
|
|
|
e8fd09 |
|
|
|
e8fd09 |
_disconnectWorkspaceSignals: function() {
|
|
|
e8fd09 |
@@ -1177,6 +1193,7 @@ const WindowList = new Lang.Class({
|
|
|
e8fd09 |
|
|
|
e8fd09 |
_onDestroy: function() {
|
|
|
e8fd09 |
this._workspaceSettings.disconnect(this._workspacesOnlyOnPrimaryChangedId);
|
|
|
e8fd09 |
+ this._dynamicWorkspacesSettings.disconnect(this._dynamicWorkspacesChangedId);
|
|
|
e8fd09 |
|
|
|
e8fd09 |
this._workspaceIndicator.destroy();
|
|
|
e8fd09 |
|
|
|
e8fd09 |
--
|
|
|
e8fd09 |
2.12.0
|
|
|
e8fd09 |
|