1 // Closes the selected dashboard tab
2 function webdeveloper_closeDashboardTab()
4 var tabBox
= document
.getElementById("webdeveloper-dashboard-tab-box");
5 var selectedTabPanel
= tabBox
.selectedPanel
;
6 var tabPanels
= document
.getElementById("webdeveloper-dashboard-tab-panels");
7 var tabs
= document
.getElementById("webdeveloper-dashboard-tabs");
9 // If the selected tab panel is set
12 tabPanels
.removeChild(selectedTabPanel
);
16 tabPanels
.removeChild(tabPanels
.childNodes
[tabBox
.selectedIndex
]);
19 tabs
.removeChild(tabBox
.selectedTab
);
21 // If there are no tab panels remaining
22 if(tabPanels
.childNodes
.length
== 0)
24 document
.getElementById("webdeveloper-dashboard").hidden
= true;
25 document
.getElementById("webdeveloper-dashboard-splitter").hidden
= true;
29 tabs
.selectedIndex
= 0;
33 // Closes the given tab in the dashboard
34 function webdeveloper_closeInDashboard(title
)
38 var tabPanels
= document
.getElementById("webdeveloper-dashboard-tab-panels");
39 var tabs
= document
.getElementById("webdeveloper-dashboard-tabs");
40 var tabElements
= tabs
.childNodes
;
41 var tabsLength
= tabElements
.length
;
43 // Loop through the tabs
44 for(var i
= 0; i
< tabsLength
; i
++)
46 tab
= tabElements
.item(i
);
49 if(tab
.nodeName
== "tab")
51 // If the tab has a matching label attribute
52 if(tab
.hasAttribute("label") && tab
.getAttribute("label") == title
)
61 // If a tab was matched
62 if(position
< tabsLength
)
64 tabPanels
.removeChild(tabPanels
.childNodes
[position
]);
65 tabs
.removeItemAt(position
);
67 // If there are no tab panels remaining
68 if(tabPanels
.childNodes
.length
== 0)
70 document
.getElementById("webdeveloper-dashboard").hidden
= true;
71 document
.getElementById("webdeveloper-dashboard-splitter").hidden
= true;
75 tabs
.selectedIndex
= 0;
80 // Returns the document for given tab in the dashboard
81 function webdeveloper_getDocumentInDashboard(title
)
85 var tabPanels
= document
.getElementById("webdeveloper-dashboard-tab-panels");
86 var tabs
= document
.getElementById("webdeveloper-dashboard-tabs");
87 var tabElements
= tabs
.childNodes
;
88 var tabsLength
= tabElements
.length
;
90 // Loop through the tabs
91 for(var i
= 0; i
< tabsLength
; i
++)
93 tab
= tabElements
.item(i
);
96 if(tab
.nodeName
== "tab")
98 // If the tab has a matching label attribute
99 if(tab
.hasAttribute("label") && tab
.getAttribute("label") == title
)
108 // If a tab was matched
109 if(position
< tabsLength
)
111 return tabPanels
.childNodes
[position
].childNodes
[0].contentDocument
;
117 // Is the given tab open in the dashboard
118 function webdeveloper_isOpenInDashboard(title
)
121 var tabs
= document
.getElementById("webdeveloper-dashboard-tabs").childNodes
;
122 var tabsLength
= tabs
.length
;
124 // Loop through the tabs
125 for(var i
= 0; i
< tabsLength
; i
++)
129 // If this is a tab and it has a matching label attribute
130 if(tab
.nodeName
== "tab" && tab
.hasAttribute("label") && tab
.getAttribute("label") == title
)
139 // Opens the given URL in the dashboard
140 function webdeveloper_openInDashboard(title
, url
)
142 var browser
= document
.createElement("browser");
143 var tab
= document
.createElement("tab");
145 var tabPanel
= document
.createElement("tabpanel");
146 var tabPanels
= document
.getElementById("webdeveloper-dashboard-tab-panels");
147 var tabs
= document
.getElementById("webdeveloper-dashboard-tabs");
149 browser
.setAttribute("flex", "1");
150 browser
.setAttribute("src", url
);
151 tabPanel
.appendChild(browser
);
152 tab
.setAttribute("label", title
);
154 tabPanels
.appendChild(tabPanel
);
155 tabs
.insertBefore(tab
, document
.getElementById("webdeveloper-dashboard-spacer"));
157 tabCount
= tabPanels
.childNodes
.length
- 1;
158 tabs
.selectedIndex
= tabCount
;
160 // If this is the only tab
163 var dashboard
= document
.getElementById("webdeveloper-dashboard");
165 // If the dashboard height is less than 100
166 if(dashboard
.height
< 100)
168 dashboard
.height
= 100;
171 // If the dashboard width is less than 100
172 if(dashboard
.width
< 100)
174 dashboard
.width
= 100;
177 dashboard
.hidden
= false;
178 document
.getElementById("webdeveloper-dashboard-splitter").hidden
= false;
182 // Positions the dashboard
183 function webdeveloper_positionDashboard()
185 var currentPosition
= webdeveloper_getStringPreference("webdeveloper.dashboard.position", true);
186 var dashboard
= document
.getElementById("webdeveloper-dashboard");
187 var dashboardSplitter
= document
.getElementById("webdeveloper-dashboard-splitter");
189 dashboard
.hidden
= true;
190 dashboardSplitter
.hidden
= true;
192 // If the current position is bottom
193 if(currentPosition
== "bottom")
195 webdeveloper_setStringPreference("webdeveloper.dashboard.position", "left");
196 webdeveloper_setupDashboardPosition("left");
198 else if(currentPosition
== "left")
200 webdeveloper_setStringPreference("webdeveloper.dashboard.position", "top");
201 webdeveloper_setupDashboardPosition("top");
203 else if(currentPosition
== "right")
205 webdeveloper_setStringPreference("webdeveloper.dashboard.position", "bottom");
206 webdeveloper_setupDashboardPosition("bottom");
208 else if(currentPosition
== "top")
210 webdeveloper_setStringPreference("webdeveloper.dashboard.position", "right");
211 webdeveloper_setupDashboardPosition("right");
214 dashboard
.hidden
= false;
215 dashboardSplitter
.hidden
= false;
218 // Selects the given tab in the dashboard
219 function webdeveloper_selectInDashboard(title
)
222 var tabs
= document
.getElementById("webdeveloper-dashboard-tabs").childNodes
;
223 var tabsLength
= tabs
.length
;
225 // Loop through the tabs
226 for(var i
= 0; i
< tabsLength
; i
++)
230 // If this is a tab and it has a matching label attribute
231 if(tab
.nodeName
== "tab" && tab
.hasAttribute("label") && tab
.getAttribute("label") == title
)
233 tabs
.selectedIndex
= i
;
240 // Sets up the dashboard position
241 function webdeveloper_setupDashboardPosition(position
)
243 var appContent
= document
.getElementById("appcontent");
244 var dashboard
= document
.getElementById("webdeveloper-dashboard");
245 var dashboardSplitter
= document
.getElementById("webdeveloper-dashboard-splitter");
247 // If the current position is bottom
248 if(position
== "bottom")
250 appContent
.appendChild(dashboardSplitter
);
251 appContent
.appendChild(dashboard
);
253 else if(position
== "left")
255 var browser
= appContent
.parentNode
;
257 browser
.insertBefore(dashboard
, appContent
);
258 browser
.insertBefore(dashboardSplitter
, appContent
);
260 else if(position
== "right")
262 webdeveloper_insertAfter(dashboard
, appContent
);
263 webdeveloper_insertAfter(dashboardSplitter
, appContent
);
265 else if(position
== "top")
267 webdeveloper_insertAsFirstChild(appContent
, dashboardSplitter
);
268 webdeveloper_insertAsFirstChild(appContent
, dashboard
);
271 // If the position is bottom or top
272 if(position
== "bottom" || position
== "top")
274 dashboardSplitter
.setAttribute("orient", "vertical");
276 else if((position
== "left" || position
== "right") && dashboardSplitter
.hasAttribute("orient"))
278 dashboardSplitter
.removeAttribute("orient");