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); |
