body{white-space:pre-wrap;} div.l0{color:#000000;} /* All debug levels. */ div.l1{color:#666666;} /* Misc. */ div.l2{color:#000000;} /* Information. */ div.l3{color:#660000;} /* Warnings. */ div.l4{color:#FF0000;} /* Errors. */ div.l5{color:#FF0000;font-weight:bold;} /* Fatal errors. */ div#pause~div{display:none;} body.l1 div.l0{display:none;} body.l2 div.l0,body.l2 div.l1{display:none;} body.l3 div.l0,body.l3 div.l1,body.l3 div.l2{display:none;} body.l4 div.l0,body.l4 div.l1,body.l4 div.l2,body.l4 div.l3{display:none;} body.l5 div.l0,body.l5 div.l1,body.l5 div.l2,body.l5 div.l3,body.l5 div.l4{display:none;} span.regex{background-color:#ffafaf;font-weight:bold;} return ( document.body.scrollTop >= ( document.body.offsetHeight - ( window.innerHeight * 1.5 ) ) ); function scrollToBottom() { document.body.scrollTop = document.body.offsetHeight; var scroll = nearBottom(); /* Remove highlighting SPANs */ list = document.getElementsByClassName('regex'); var parent = span.parentNode; var content = span.textContent; var text = document.createTextNode(content); parent.replaceChild(text, span); list = document.getElementsByClassName('hide'); list[i].classList.remove('hide'); highlightTextNodes: function (div, start_pos, end_pos) { var data = [], node, range, span, contents; var this_start, this_end; /* First, find the container nodes and offsets to apply highlighting. */ if (node.nodeType === Node.TEXT_NODE) { end_ind = ind + node.length; else if (start_pos < end_ind) this_start = start_pos - ind; this_end = end_pos - ind; this_end = end_ind - ind; if (this_start != -1 && this_start < this_end) { data.push(this_end, this_start, node); if (node.hasChildNodes()) { var next = node.nextSibling; /* Second, apply highlighting to saved sections. Changing the DOM is automatically reflected in all WebKit API, so we have to do this after finding the offsets, or things could get complicated. */ range = document.createRange(); range.setStart(node, this_start); range.setEnd(node, this_end); span = document.createElement('span'); span.className = 'regex'; contents = range.extractContents(); span.appendChild(contents); var m, count, start_pos, end_pos; /* We do a first pass to see if it matches at all. If it does we work out * the offsets to highlight. this.regex.lastIndex = 0; var match_info = this.regex.exec(text); if ((match_info != null) != this.invert) { /* If we're not highlighting or the expression is inverted, we're if (!this.highlight || this.invert) count = match_info.length; /* We do this because JS doesn't provide a sufficient means to determine the indices of matched groups. So we're just going to highlight the entire match instead. */ start_pos = match_info.index; end_pos = this.regex.lastIndex; this.highlightTextNodes(div, start_pos, end_pos); /* Workaround broken API for empty matches */ if (match_info.index == this.regex.lastIndex) } while (match_info = this.regex.exec(text)); div.classList.add('hide'); filterAll: function (str, inv, high) { this.regex = new RegExp(str, 'gi'); var list = document.getElementsByTagName('div'); for (var i = 0; i < list.length; i++) function append(level, time, cat, msg) { var div = document.createElement('div'); div.className = 'l' + level; div.appendChild(document.createTextNode('(' + time + ') ')); var cat_n = document.createElement('b'); cat_n.appendChild(document.createTextNode(cat + ':')); div.appendChild(document.createTextNode(' ')); div.appendChild(document.createTextNode(msg)); var scroll = nearBottom(); document.body.appendChild(div); document.body.innerHTML = ''; document.body.insertAdjacentHTML('beforeEnd', '<div id=pause></div>'); function resumeOutput() { var pause = document.getElementById('pause'); var parent = pause.parentNode; parent.removeChild(pause); function setFilterLevel(l) { var scroll = nearBottom(); document.body.className = 'l'+l;