summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBrian Cully <bjc@spork.org>2025-08-24 12:19:45 -0400
committerBrian Cully <bjc@spork.org>2025-08-24 12:32:15 -0400
commit57f32dc1d36650a5f282f1ba3906e9772b89709d (patch)
treeb967e413bdb4cf4cf82c2c9aed60bb77baee3a40
parentddf944d808c71946a67d21d9fd1268ca05b787d1 (diff)
downloadautomathon-57f32dc1d36650a5f282f1ba3906e9772b89709d.tar.gz
automathon-57f32dc1d36650a5f282f1ba3906e9772b89709d.zip
use css custom highlights for in-text blinken
-rw-r--r--index.html5
-rw-r--r--main.css3
-rw-r--r--main.mjs24
3 files changed, 12 insertions, 20 deletions
diff --git a/index.html b/index.html
index 0882b65..77c2bdc 100644
--- a/index.html
+++ b/index.html
@@ -12,15 +12,14 @@
<div id='code'>
<button id='compile'>compile</button>
<br>
- <pre id='src' contenteditable='plaintext-only'>
-: fac
+ <div id='src' contenteditable='plaintext-only'>: fac
dup
1 > if
dup 1 - fac *
then
;
5 fac
-drop</pre>
+drop</div>
</div>
<div id='state-container'>
diff --git a/main.css b/main.css
index a1ea31a..9f7381d 100644
--- a/main.css
+++ b/main.css
@@ -22,9 +22,10 @@ html {
margin-top: 1ex;
padding: 1em;
border: 2px inset lightgray;
+ white-space: pre-wrap;
}
-#src .exec {
+::highlight(exec) {
background-color: yellowgreen;
}
diff --git a/main.mjs b/main.mjs
index 801736e..701659f 100644
--- a/main.mjs
+++ b/main.mjs
@@ -55,26 +55,18 @@ function renderCallStack(interp) {
});
}
+const highRange = new Range();
+const highlight = new Highlight(highRange);
+CSS.highlights.set('exec', highlight);
+
function renderTextHighlight(interp) {
const ip = interp.ip();
const anno = interp.annotation_at(ip)
- const src = document.querySelector('#src')
- const text = src.textContent;
-
- // split textcontent into 3 spans: pre-highlight, highlight,
- // post-highlight
- const pre = document.createElement('span');
- pre.textContent = text.substring(0, anno.start);
- const high = document.createElement('span');
- high.classList.add('exec');
- high.textContent = text.substring(anno.start, anno.end);
- const post = document.createElement('span');
- post.textContent = text.substring(anno.end);
+ const src = document.querySelector('#src');
- while (src.lastChild) { src.removeChild(src.lastChild) }
- src.appendChild(pre);
- src.appendChild(high);
- src.appendChild(post);
+ // this assumes the text node is the first child, maybe it isn't?
+ highRange.setStart(src.childNodes[0], anno.start);
+ highRange.setEnd(src.childNodes[0], anno.end);
}
function tick(interp) {