// Portal Highlighter //////////////////////////////////////////////////////////
// these functions handle portal highlighters
window._highlighters = null;
window._current_highlighter = localStorage.portal_highlighter;
window.changing_highlighters = false;
window._no_highlighter = 'No Highlights';
window.addPortalHighlighter = function(name, callback) {
if(_highlighters === null) {
_highlighters = {};
}
_highlighters[name] = callback;
if(localStorage.portal_highlighter === undefined) {
_current_highlighter = name;
localStorage.portal_highlighter = name;
}
portalHighlighterControl();
}
window.portalHighlighterControl = function() {
if(_highlighters !== null) {
if($('#portal_highlight_select').length === 0) {
$("body").append("");
}
$("#portal_highlight_select").html('');
$("#portal_highlight_select").append($("