diff options
author | Adam Chlipala <adam@chlipala.net> | 2019-07-17 14:28:46 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2019-07-17 14:28:46 -0400 |
commit | e16efaf6603c4da33b74b499e0e1214c46ddf72d (patch) | |
tree | d90b5d5cca43095f27b3f8c959791941f5e2d107 /lib/js | |
parent | 7fbfe759d3bc572dd7ee379429f0ff2d1f7894a0 (diff) |
New JavaScript FFI function 'listen'
Diffstat (limited to 'lib/js')
-rw-r--r-- | lib/js/urweb.js | 10 |
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; |