Merge WebKit at r73109: Initial merge by git.

[android-x86/external-webkit.git] / WebKit / chromium / src / js / DevTools.js

diff --git a/WebKit/chromium/src/js/DevTools.js b/WebKit/chromium/src/js/DevTools.js
index a66e174..5bb150c 100644 (file)
--- a/WebKit/chromium/src/js/DevTools.js
+++ b/WebKit/chromium/src/js/DevTools.js
@@ -46,6 +46,9 @@ var context = {};  // Used by WebCore's inspector routines.
     Preferences.canEditScriptSource = true;
     Preferences.onlineDetectionEnabled = false;
     Preferences.nativeInstrumentationEnabled = true;
+    Preferences.fileSystemEnabled = false;
+    Preferences.showTimingTab = true;
+    Preferences.showCookiesTab = true;
 })();
 
 var devtools = devtools || {};
@@ -162,3 +165,25 @@ WebInspector.resetToolbarColors = function()
 
 }
 
+////////////////////////////////////////////////////////
+// Platform-specific WebInspector extensions support. //
+////////////////////////////////////////////////////////
+
+WebInspector.platformExtensionAPI = function(tabId)
+{
+    function getTabId()
+    {
+        return tabId;
+    }
+    webInspector.inspectedWindow.__proto__.__defineGetter__("tabId", getTabId);
+}
+
+WebInspector.buildPlatformExtensionAPI = function()
+{
+    return "(" + WebInspector.platformExtensionAPI + ")(" + WebInspector._inspectedTabId + ");";
+}
+
+WebInspector.setInspectedTabId = function(tabId)
+{
+    WebInspector._inspectedTabId = tabId;
+}