DevTools: mute accidental refresh requests while on DevTools window.

webkit/glue/devtools/js/devtools.js

 // Copyright (c) 2009 The Chromium Authors. All rights reserved.
 // Use of this source code is governed by a BSD-style license that can be
 // found in the LICENSE file.
 
 /**
  * @fileoverview Tools is a main class that wires all components of the
  * DevTools frontend together. It is also responsible for overriding existing
  * WebInspector functionality while it is getting upstreamed into WebCore.
  */
 goog.provide('devtools.Tools');
@@ skipping 204 matching lines @@
 ///////////////////////////////////////////////////////////////////////////////
 // Here and below are overrides to existing WebInspector methods only.
 // TODO(pfeldman): Patch WebCore and upstream changes.
 var oldLoaded = WebInspector.loaded;
 WebInspector.loaded = function() {
   devtools.tools = new devtools.ToolsAgent();
   devtools.tools.reset();
 
   Preferences.ignoreWhitespace = false;
   oldLoaded.call(this);
+
+  // Hide dock button on Mac OS.
+  // TODO(pfeldman): remove once Mac OS docking is implemented.
   if (InspectorController.platform().indexOf('mac') == 0) {
     document.getElementById('dock-status-bar-item').addStyleClass('hidden');
   }
 
+  // Mute refresh action.
+  document.addEventListener("keydown", function(event) {
+    if (event.keyIdentifier == 'F5') {
+      event.preventDefault();
+    } else if (event.keyIdentifier == 'U+0052' &&

[yurys, 2009/07/21 12:01:36]

please use a constant for this

+        (event.ctrlKey || event.metaKey)) {
+      event.preventDefault();
+    }
+  }, true);
+
   DevToolsHost.loaded();
 };
 
 
 var webkitUpdateChildren =
     WebInspector.ElementsTreeElement.prototype.updateChildren;
 
 
 /**
  * @override
@@ skipping 811 matching lines @@
   };
 
   var originalDragEnd = WebInspector.elementDragEnd;
   WebInspector.elementDragEnd = function() {
     originalDragEnd.apply(this, arguments);
 
     var glassPane = document.getElementById('glass-pane-for-drag');
     glassPane.parentElement.removeChild(glassPane);
   };
 })();