|
|
|
@ -200,9 +200,16 @@ function clear(ctx) {
@@ -200,9 +200,16 @@ function clear(ctx) {
|
|
|
|
|
ctx.restore(); |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
/* Auto-scroll if the scrollbar is near the bottom, otherwise do nothing. */ |
|
|
|
|
function checkScrolling() { |
|
|
|
|
if ((stdout.scrollHeight - stdout.scrollTop) <= stdout.offsetHeight) { |
|
|
|
|
stdout.scrollTop = stdout.scrollHeight; |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
function log(str) { |
|
|
|
|
stdout.innerHTML += str; |
|
|
|
|
window.scrollTo(0, stdout.getBoundingClientRect().bottom); |
|
|
|
|
checkScrolling(); |
|
|
|
|
} |
|
|
|
|
</script> |
|
|
|
|
</head> |
|
|
|
|