summaryrefslogtreecommitdiff
path: root/lib/js
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2019-07-17 14:28:46 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2019-07-17 14:28:46 -0400
commite16efaf6603c4da33b74b499e0e1214c46ddf72d (patch)
treed90b5d5cca43095f27b3f8c959791941f5e2d107 /lib/js
parent7fbfe759d3bc572dd7ee379429f0ff2d1f7894a0 (diff)
New JavaScript FFI function 'listen'
Diffstat (limited to 'lib/js')
-rw-r--r--lib/js/urweb.js10
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 66d427c8..332de6dc 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -2135,6 +2135,16 @@ function active(s) {
}
}
+function listen(s, onchange) {
+ var x = document.createElement("script");
+ x.dead = false;
+ x.signal = s;
+ x.sources = null;
+ x.closures = null;
+ x.recreate = onchange;
+ populate(x);
+}
+
function input(x, s, recreate, type, name) {
if (name) x.name = name;
if (type) x.type = type;