From 5052c6d3504442db6342d56d14367e26451dc8d6 Mon Sep 17 00:00:00 2001 From: Giovanni Campagna Date: Wed, 1 May 2013 00:45:06 +0200 Subject: [PATCH] windowsNavigator: update for gnome-shell changes The position of a workspace is not part of a geometry object. --- extensions/windowsNavigator/extension.js | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/extensions/windowsNavigator/extension.js b/extensions/windowsNavigator/extension.js index 50beaa85..7b75d415 100644 --- a/extensions/windowsNavigator/extension.js +++ b/extensions/windowsNavigator/extension.js @@ -47,11 +47,23 @@ function enable() { winInjections['hideTooltip'] = undefined; Workspace.Workspace.prototype.showTooltip = function() { - if (this._tip == null) + if (this._tip == null || this._actualGeometry == null) return; this._tip.text = (this.metaWorkspace.index() + 1).toString(); - this._tip.x = this._x; - this._tip.y = this._y; + + // Hand code this instead of using _getSpacingAndPadding + // because that fails on empty workspaces + let node = this.actor.get_theme_node(); + let padding = { + left: node.get_padding(St.Side.LEFT), + top: node.get_padding(St.Side.TOP), + bottom: node.get_padding(St.Side.BOTTOM), + right: node.get_padding(St.Side.RIGHT), + }; + + let area = Workspace.padArea(this._actualGeometry, padding); + this._tip.x = area.x; + this._tip.y = area.y; this._tip.show(); this._tip.raise_top(); }