fix +7506 Tabs are not rendered correctly on firefox

package.json

@@ -108,7 +108,7 @@
         "c9.ide.run.debug.xdebug": "#3b1520f83d",
         "c9.ide.save": "#58b8616a88",
         "c9.ide.terminal.monitor": "#b0b4d03280",
-        "c9.ide.theme.flat": "#b1d65fa9bb",
+        "c9.ide.theme.flat": "#2de8414db7",
         "c9.ide.threewaymerge": "#229382aa0b",
         "c9.ide.undo": "#b028bcb4d5",
         "c9.ide.upload": "#0bd010d3dc",

plugins/c9.ide.layout.classic/layout.js

@@ -35,7 +35,7 @@ define(function(require, exports, module) {
         
         var logobar, removeTheme, theme;
         var c9console, menus, tabManager, panels;
-        var userLayout, ignoreTheme, notify;
+        var userLayout, ignoreTheme, notify, svg;
         
         var loaded = false;
         function load(){
@@ -129,6 +129,8 @@ define(function(require, exports, module) {
             window.addEventListener("resize", resize, false);
             window.addEventListener("focus", resize, false);
             
+            setGeckoMask();
+            
             plugin.addOther(function(){
                 window.removeEventListener("resize", resize, false);
                 window.removeEventListener("focus", resize, false);
@@ -190,6 +192,8 @@ define(function(require, exports, module) {
                     type: type
                 }) !== false;
                 
+                setGeckoMask();
+                
                 if (noquestion) return;
                 
                 if (auto)
@@ -230,6 +234,37 @@ define(function(require, exports, module) {
         
         /***** Methods *****/
         
+        // There will be a better place for this when theming is fully
+        // abstracted. For now this is a hack
+        function setGeckoMask(){
+            if (!apf.isGecko) return;
+            
+            if (svg) svg.parentNode.removeChild(svg);
+            
+            var isFlatTheme = theme.indexOf("flat") > -1;
+            var img = options.staticPrefix + "/images/" + (
+                isFlatTheme
+                    ? "gecko_mask_flat_light.png"
+                    : "gecko_mask.png");
+            var width = isFlatTheme ? 76 : 46;
+            var height = isFlatTheme ? 26 : 24;
+            var x1 = isFlatTheme ? 1 : 1;
+            var x2 = isFlatTheme ? -40 : -28;
+            
+            document.body.insertAdjacentHTML("beforeend", '<svg xmlns="http://www.w3.org/2000/svg">'
+                + '<defs>'
+                    + '<mask id="tab-mask-left" maskUnits="userSpaceOnUse" maskContentUnits="userSpaceOnUse">'
+                        + '<image width="' + width + 'px" height="' + height + 'px" xlink:href="' + img + '" x="' + x1 + 'px"></image>'
+                    + '</mask>'
+                    + '<mask id="tab-mask-right" maskUnits="userSpaceOnUse" maskContentUnits="userSpaceOnUse">'
+                        + '<image width="' + width + 'px" height="' + height + 'px" xlink:href="' + img + '" x="' + x2 + 'px"></image>'
+                    + '</mask>'
+                + '</defs>'
+            + '</svg>');
+            
+            svg = document.body.lastChild;
+        }
+        
         function findParent(obj, where) {
             if (obj.name == "menus") {
                 menus = obj;
@@ -530,6 +565,10 @@ define(function(require, exports, module) {
             activeFindArea = null;
             defaultFindArea = null;
             activating = null;
+            
+            if (svg && svg.parentNode)
+                svg.parentNode.removeChild(svg);
+            svg = null;
         });
         
         /***** Register and define API *****/