comparison lib/js/urweb.js @ 1555:d5c961c709f9

New client-side, document-level event handlers
author Adam Chlipala <adam@chlipala.net>
date Sat, 03 Sep 2011 11:48:12 -0400
parents 4105f779de7b
children e1f5d9c4cc20
comparison
equal deleted inserted replaced
1554:396e8d881205 1555:d5c961c709f9
198 serverHandlers = cons(f, serverHandlers); 198 serverHandlers = cons(f, serverHandlers);
199 } 199 }
200 200
201 function servErr(s) { 201 function servErr(s) {
202 window.setTimeout(function () { runHandlers("Server", serverHandlers, s); }, 0); 202 window.setTimeout(function () { runHandlers("Server", serverHandlers, s); }, 0);
203 }
204
205 // Key events
206
207 var uw_event = null;
208
209 function kc() {
210 return window.event ? event.keyCode : (uw_event ? uw_event.which : 0);
211 }
212
213 // Document events
214
215 function uw_handler(name, f) {
216 var old = document[name];
217 if (old == undefined)
218 document[name] = function() { execF(f); return false; };
219 else
220 document[name] = function() { old(); execF(f); return false; };
221 }
222
223 function uw_onClick(f) {
224 uw_handler("onclick", f);
225 }
226
227 function uw_onDblclick(f) {
228 uw_handler("ondblclick", f);
229 }
230
231 function uw_onMousedown(f) {
232 uw_handler("onmousedown", f);
233 }
234
235 function uw_onMouseup(f) {
236 uw_handler("onmouseup", f);
237 }
238
239 function uw_keyHandler(name, f) {
240 var old = document[name];
241 if (old == undefined)
242 document[name] = function(event) { uw_event = event; execF(execF(f, kc())); return false; };
243 else
244 document[name] = function(event) { uw_event = event; old(); execF(execF(f, kc())); return false; };
245 }
246
247 function uw_onKeydown(f) {
248 uw_keyHandler("onkeydown", f);
249 }
250
251 function uw_onKeypress(f) {
252 uw_keyHandler("onkeypress", f);
253 }
254
255 function uw_onKeyup(f) {
256 uw_keyHandler("onkeyup", f);
203 } 257 }
204 258
205 259
206 // Embedding closures in XML strings 260 // Embedding closures in XML strings
207 261
1020 window.setTimeout(function() { k(null); }, ms); 1074 window.setTimeout(function() { k(null); }, ms);
1021 } 1075 }
1022 1076
1023 function sp(e) { 1077 function sp(e) {
1024 execF(e, null); 1078 execF(e, null);
1025 }
1026
1027
1028 // Key events
1029
1030 var uw_event = null;
1031
1032 function kc() {
1033 return window.event ? event.keyCode : (uw_event ? uw_event.keyCode : 0);
1034 } 1079 }
1035 1080
1036 1081
1037 // The Ur interpreter 1082 // The Ur interpreter
1038 1083