[gnome-shell-extensions] windowsNavigator: update for gnome-shell changes

[Giovanni Campagna <gcampagna src gnome org>]

commit 5052c6d3504442db6342d56d14367e26451dc8d6
Author: Giovanni Campagna <gcampagna src gnome org>
Date:   Wed May 1 00:45:06 2013 +0200

    windowsNavigator: update for gnome-shell changes
    
    The position of a workspace is not part of a geometry object.

 extensions/windowsNavigator/extension.js |   18 +++++++++++++++---
 1 files changed, 15 insertions(+), 3 deletions(-)
---
diff --git a/extensions/windowsNavigator/extension.js b/extensions/windowsNavigator/extension.js
index 50beaa8..7b75d41 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();
     }