diff options
| author | Jez Ng | 2012-03-03 03:11:25 -0500 | 
|---|---|---|
| committer | Jez Ng | 2012-03-06 08:43:10 -0500 | 
| commit | e9366ac22ed32ef54cf949acc9f63190b04c5773 (patch) | |
| tree | 02871cb32f4494eb2826087f49d27ef68aad717a | |
| parent | 8d85fef79ea1e50106df47f4ae652e7c4dd0f07d (diff) | |
| download | vimium-e9366ac22ed32ef54cf949acc9f63190b04c5773.tar.bz2 | |
Further reduction in state -- cssAdded is unnecessary.
| -rw-r--r-- | linkHints.js | 7 | ||||
| -rw-r--r-- | vimiumFrontend.js | 3 | 
2 files changed, 4 insertions, 6 deletions
diff --git a/linkHints.js b/linkHints.js index 5a8cee13..3b3fc3f9 100644 --- a/linkHints.js +++ b/linkHints.js @@ -18,8 +18,6 @@ var linkHints = {    linkActivator: undefined,    // Whether link hint's "open in current/new tab" setting is currently toggled    openLinkModeToggle: false, -  // Whether we have added to the page the CSS needed to display link hints. -  cssAdded: false,    // While in delayMode, all keypresses have no effect.    delayMode: false,    // Handle the link hinting marker generation and matching. Must be initialized after settings have been @@ -54,10 +52,9 @@ var linkHints = {    activateModeWithQueue: function() { this.activateMode(true, true, false); },    activateMode: function(openInNewTab, withQueue, copyLinkUrl) { -    if (!this.cssAdded) +    if (!document.getElementById('vimiumLinkHintCss'))        // linkHintCss is declared by vimiumFrontend.js and contains the user supplied css overrides. -      addCssToPage(linkHintCss);  -    this.cssAdded = true; +      addCssToPage(linkHintCss, 'vimiumLinkHintCss');      this.setOpenLinkMode(openInNewTab, withQueue, copyLinkUrl);      this.buildLinkHints();      handlerStack.push({ // modeKeyHandler is declared by vimiumFrontend.js diff --git a/vimiumFrontend.js b/vimiumFrontend.js index cc7065c0..80881d84 100644 --- a/vimiumFrontend.js +++ b/vimiumFrontend.js @@ -1141,13 +1141,14 @@ Tween = {  /*   * Adds the given CSS to the page.   */ -function addCssToPage(css) { +function addCssToPage(css, id) {    var head = document.getElementsByTagName("head")[0];    if (!head) {      head = document.createElement("head");      document.documentElement.appendChild(head);    }    var style = document.createElement("style"); +  style.id = id;    style.type = "text/css";    style.appendChild(document.createTextNode(css));    head.appendChild(style);  | 
