background-color: #9C9CFF;
}
+.cm-s-mozilla .cm-unused-line {
+ text-decoration: line-through;
+ -moz-text-decoration-color: #8050B0;
+}
+
+.cm-s-mozilla .cm-executed-line {
+ background-color: #404000;
+}
+
.theme-fg-color3,
.cm-s-mozilla .cm-builtin,
.cm-s-mozilla .cm-tag,
border-bottom: 1px solid #A09090;
}
-.theme-tooltip-panel .devtools-tooltip-font-previewer-text {
- color: FF9F00;
-}
-
.theme-tooltip-panel .devtools-tooltip-simple-text:last-child {
border-bottom: 0;
}
* Rules that apply to the global toolbox like command buttons,
* devtools tabs, docking buttons, etc. */
-#toolbox-controls {
- margin: 0 2px;
-}
-
#toolbox-controls > toolbarbutton,
#toolbox-dock-buttons > toolbarbutton {
min-width: 16px;
}
#toolbox-controls-separator {
- -moz-margin-start: 4px;
+ width: 2px;
+}
+
+#toolbox-controls-separator[invisible] {
+ visibility: hidden;
}
/* Command buttons */
border-radius: 8px 8px 0 0;
}
-.devtools-tab:first-child {
-}
-
-.devtools-tab:last-child {
-}
-
.devtools-tab > image {
-moz-margin-end: 0px;
/* -moz-margin-start: 4px; */
width: 16px; /* Prevents collapse during theme switching */
}
-#toolbox-tab-options > image {
-/* margin: 0 8px; */
-}
-
.devtools-tab:hover > image {
}
visibility: collapse;
}
+/* The options tab is special - it doesn't have the same parent
+ as the other tabs (toolbox-option-container vs toolbox-tabs) */
+#toolbox-option-container .devtools-tab:not([selected]) {
+/* background-color: transparent;*/
+}
+#toolbox-option-container .devtools-tab {
+/* border-color: transparent;
+ border-width: 0;
+ -moz-padding-start: 1px;*/
+}
+#toolbox-tab-options > image {
+/* margin: 0 8px;*/
+}
+
.hidden-labels-box:not(.visible) > label,
.hidden-labels-box.visible ~ .hidden-labels-box > label:last-child {
display: none;