/* A list of input fields which might need periodic kicking. */
var KICK_INPUT_FIELDS = [];
+function input_widget(id, dep, kickfn) {
+ /* Bind an input widget (with the given ID) to a DEP, calling KICKFN (with
+ * the widget element as its argument) to update DEP from the state of the
+ * widget. This is common machinery for `input_field' and `input_radio'.
+ */
+
+ var e = elt(id);
+
+ // 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.
*/
- var e = elt(id);
-
- function kick() {
- /* Update the dep from the element content. If the convert function
+ input_widget(id, dep, function (e) {
+ /* Update the dep from the element content. If the CONVERT function
* doesn't like the input then mark the dep as bad and highlight the
* input element.
*/
dep.make_bad();
add_elt_class(e, 'bad');
}
- }
-
- // Name the dep after our id.
- dep.name = id;
-
- // Arrange to update the dep `shortly after' updates.
- var soon = new Soon(kick);
- function kick_soon() { soon.kick(); }
- e.addEventListener('click', kick_soon, false);
- e.addEventListener('blur', kick_soon, false);
- e.addEventListener('keypress', kick_soon, false);
-
- // Sadly, the collection of events above isn't comprehensive, because we
- // don't actually get told about edits as a result of clipboard operations,
- // or even (sometimes) deletes, so add our `kick' function to a list of
- // such functions to be run periodically just in case.
- KICK_INPUT_FIELDS.push(kick);
+ });
}
DEP_UI.input_field = input_field;
* the button, set the dep to the element's `value' attribute.
*/
- var e = elt(id);
-
- function kick() {
- // Make sure we're actually chosen. We get called periodically
- // regardless of user input.
+ input_widget(id, dep, function (e) {
+ // Make sure we're actually chosen. We might get called regardless of
+ // user input.
if (e.checked) dep.set_value(e.value);
- };
-
- // Name the dep after our id.
- dep.name = id;
-
- // Arrange to update the dep `shortly after' updates.
- var soon = new Soon(kick);
- function kick_soon() { soon.kick(); }
- e.addEventListener('click', kick_soon, false);
- e.addEventListener('changed', kick_soon, false);
-
- // The situation for radio buttons doesn't seem as bad as for text widgets,
- // but let's be on the safe side.
- KICK_INPUT_FIELDS.push(kick);
+ });
}
DEP_UI.input_radio = input_radio;
DEP.dolist(KICK_INPUT_FIELDS, function (func) { func(); });
}
-// Update the input fields relatively frequently.
-setInterval(kick_all, 500);
-
// And make sure we get everything started when the page is fully loaded.
window.addEventListener('load', kick_all, false);