DevTools: [Sources] Improve editor load time by optimizing setMimeType

third_party/WebKit/Source/devtools/front_end/externs.js

 /*
  * Copyright (C) 2011 Google Inc. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are
  * met:
  *
  *     * Redistributions of source code must retain the above copyright
  * notice, this list of conditions and the following disclaimer.
  *     * Redistributions in binary form must reproduce the above
@@ skipping 511 matching lines @@
   setSelections: function(selections, primaryIndex, config) {},
   setSize: function(width, height) {},
   setValue: function(code) {},
   somethingSelected: function() {},
   swapDoc: function(doc) {},
   undo: function() {},
   unlinkDoc: function(other) {}
 };
 /** @type {!{cursorDiv: Element}} */
 CodeMirror.prototype.display;
+/** @type {!{mode: string}} */
+CodeMirror.prototype.options;
 /** @type {!Object} */
 CodeMirror.Pass;
 CodeMirror.showHint = function(codeMirror, hintintFunction) {};
 CodeMirror.commands = {};
 CodeMirror.modes = {};
 CodeMirror.mimeModes = {};
 CodeMirror.getMode = function(options, spec) {};
 CodeMirror.overlayMode = function(mode1, mode2, squashSpans) {};
 CodeMirror.defineMode = function(modeName, modeConstructor) {};
 CodeMirror.startState = function(mode) {};
@@ skipping 301 matching lines @@
 var Sources = {};
 var Terminal = {};
 var TextEditor = {};
 var Timeline = {};
 var TimelineModel = {};
 var ToolboxBootstrap = {};
 var UI = {};
 var UtilitySharedWorker = {};
 var WorkerService = {};
 var Workspace = {};