[gnome-shell] Make workspace selector more similar to the mockup

[Stefano Facchini <sfacchini src gnome org>]

commit 18c62a198768d15f5d46fdd3d2a5624de1ccbe29
Author: Stefano Facchini <stefano facchini gmail com>
Date:   Sun Nov 27 00:28:51 2011 +0100

    Make workspace selector more similar to the mockup
    
    This makes the workspace indicator respect the "padding" style attribute.
    Also, since we no longer draw the border on top of the thumbnail,
    we need to be pixel-precise in allocating the indicator height.
    
    We use this to make the workspace selector more similar to the mockup.
    
    https://bugzilla.gnome.org/show_bug.cgi?id=662087

 data/theme/gnome-shell.css  |   10 ++++++----
 js/ui/workspaceThumbnail.js |   25 +++++++++++++++++++------
 2 files changed, 25 insertions(+), 10 deletions(-)
---
diff --git a/data/theme/gnome-shell.css b/data/theme/gnome-shell.css
index 6f3a612..6d78bc9 100644
--- a/data/theme/gnome-shell.css
+++ b/data/theme/gnome-shell.css
@@ -578,22 +578,24 @@ StButton.popup-menu-item:insensitive {
     border-right: 0px;
     border-radius: 9px 0px 0px 9px;
     background-color: rgba(0, 0, 0, 0.5);
-    padding: 8px;
+    padding: 11px 7px 11px 11px;
 }
 
 .workspace-thumbnails-background:rtl {
     border-right: 1px;
     border-left: 0px;
     border-radius: 0px 9px 9px 0px;
+    padding: 11px 11px 11px 7px;
 }
 
 .workspace-thumbnails {
-    spacing: 7px;
+    spacing: 11px;
 }
 
 .workspace-thumbnail-indicator {
-    outline: 2px solid white;
-    border: 1px solid #888;
+    border: 4px solid rgba(255,255,255,0.7);
+    border-radius: 4px;
+    padding: 1px;
 }
 
 .window-caption {
diff --git a/js/ui/workspaceThumbnail.js b/js/ui/workspaceThumbnail.js
index 4708a88..ab2e7ad 100644
--- a/js/ui/workspaceThumbnail.js
+++ b/js/ui/workspaceThumbnail.js
@@ -1045,9 +1045,16 @@ const ThumbnailsBox = new Lang.Class({
         childBox.y2 = box.y2;
         this._background.allocate(childBox, flags);
 
-        let indicatorY = this._indicatorY;
+        let indicatorY1 = this._indicatorY;
+        let indicatorY2;
         // when not animating, the workspace position overrides this._indicatorY
         let indicatorWorkspace = !this._animatingIndicator ? global.screen.get_active_workspace() : null;
+        let indicatorThemeNode = this._indicator.get_theme_node();
+
+        let indicatorTopFullBorder = indicatorThemeNode.get_padding(St.Side.TOP) + indicatorThemeNode.get_border_width(St.Side.TOP);
+        let indicatorBottomFullBorder = indicatorThemeNode.get_padding(St.Side.BOTTOM) + indicatorThemeNode.get_border_width(St.Side.BOTTOM);
+        let indicatorLeftFullBorder = indicatorThemeNode.get_padding(St.Side.LEFT) + indicatorThemeNode.get_border_width(St.Side.LEFT);
+        let indicatorRightFullBorder = indicatorThemeNode.get_padding(St.Side.RIGHT) + indicatorThemeNode.get_border_width(St.Side.RIGHT);
 
         let y = contentBox.y1;
 
@@ -1093,8 +1100,10 @@ const ThumbnailsBox = new Lang.Class({
             let y2 = Math.round(y + thumbnailHeight);
             let roundedVScale = (y2 - y1) / portholeHeight;
 
-            if (thumbnail.metaWorkspace == indicatorWorkspace)
-                indicatorY = y1;
+            if (thumbnail.metaWorkspace == indicatorWorkspace) {
+                indicatorY1 = y1;
+                indicatorY2 = y2;
+            }
 
             // Allocating a scaled actor is funny - x1/y1 correspond to the origin
             // of the actor, but x2/y2 are increased by the *unscaled* size.
@@ -1119,8 +1128,10 @@ const ThumbnailsBox = new Lang.Class({
             childBox.x1 = contentBox.x2 - thumbnailWidth;
             childBox.x2 = contentBox.x2;
         }
-        childBox.y1 = indicatorY;
-        childBox.y2 = childBox.y1 + thumbnailHeight;
+        childBox.x1 -= indicatorLeftFullBorder;
+        childBox.x2 += indicatorRightFullBorder;
+        childBox.y1 = indicatorY1 - indicatorTopFullBorder;
+        childBox.y2 = (indicatorY2 ? indicatorY2 : (indicatorY1 + thumbnailHeight)) + indicatorBottomFullBorder;
         this._indicator.allocate(childBox, flags);
     },
 
@@ -1135,7 +1146,9 @@ const ThumbnailsBox = new Lang.Class({
         }
 
         this._animatingIndicator = true;
-        this.indicatorY = this._indicator.allocation.y1;
+        let indicatorThemeNode = this._indicator.get_theme_node();
+        let indicatorTopFullBorder = indicatorThemeNode.get_padding(St.Side.TOP) + indicatorThemeNode.get_border_width(St.Side.TOP);
+        this.indicatorY = this._indicator.allocation.y1 + indicatorTopFullBorder;
         Tweener.addTween(this,
                          { indicatorY: thumbnail.actor.allocation.y1,
                            time: WorkspacesView.WORKSPACE_SWITCH_TIME,