+ // Name the dep after our id.
+ dep.name = id;
+
+ // Arrange to update the dep `shortly after' updates.
+ function kick() { kickfn(e); }
+ var soon = new Soon(kick);
+ function kick_soon() { soon.kick(); }
+ e.addEventListener('input', kick_soon, false);
+
+ // Set our field to the correct state when the page finishes loading.
+ KICK_INPUT_FIELDS.push(kick);
+}
+
+function input_field(id, dep, convert) {
+ /* Bind an input field (with the given ID) to a DEP, converting the user's
+ * input with the CONVERT function.
+ */
+
+ input_widget(id, dep, function (e) {
+ /* Update the dep from the element content. If the CONVERT function