#lang racket (require redex/reduction-semantics) (provide DOM DOM-reduce) ;; Version 2 ;; Annotations refer to the DOM Level 3 Events Specification, except where ;; otherwise noted. ;; (http://www.w3.org/TR/DOM-Level-3-Events/) (define (all-unique? l) (equal? (remove-duplicates l) l)) (define (not-in? T_event P LS) (empty? (filter (lambda (tp) (equal? tp (list T_event P))) LS))) (define-language DOM [bool #t #f] ; Events ; 4.1 - Event Interface ; event: type, bubbles, cancelable, trusted, metadata, default action [E (event T Bubbles Cancels Trusted Meta loc)] ; Meta: event metadata [Meta ((string any) ...)] ; T (event type): readonly attribute DOMString type; ; The name of the event type. The name must be a DOMString. Specifications ; that define events, content authors, and authoring tools must use ; case-sensitive event type names." [T string] ; Bubbles (bubbles): readonly attribute boolean bubbles; ; Used to indicate whether or not an event is a bubbling event. If the event ; can bubble the value must be true, otherwise the value must be false. [Bubbles bool] ; Cancels (cancelable): readonly attribute boolean cancelable; ; Used to indicate whether or not an event can have its default action ; prevented (see also Default actions and cancelable events). If the default ; action can be prevented the value must be true, otherwise the value must be ; false. [Cancels bool] ; Trusted (isTrusted): readonly attribute boolean isTrusted; ; Used to indicate whether this event was generated by the user agent ; (trusted) or by script (untrusted). See trusted events for more details. [Trusted bool] ; Phases ; 3.1 - Event dispatch and DOM event flow ; ... the event object must complete one or more event phases. ; This specification defines three event phases: capture phase; target phase; ; and bubble phase... [P capture target bubble] ; Locations are like pointers. The machine state maintains ; a list of (location, DOM node) pairs, followed by a list of (location, Statement) pairs. [loc (variable-prefix loc) (variable-prefix fun)] ; parent is possibly null (parent of root node) [parent null loc] ; DOM Nodes ; N: node name, listeners, children, parent [N (node string LS (loc ...) parent)] ; TP: event type, phase [TP (T P)] ; LS: a list of (TP, listener list) pairs [LS (side-condition (((name tp TP) (HL ...)) ...) (all-unique? (term (tp ...))))] ; Event Listeners ; 4.4 - EventListener interface [HL (listener bool loc) (handler S) (nullhandler)] [L (listener bool S) ;was this installed with useCapture? (handler S) (gethandler)] ; Predispatch: target node, path root->target, event [PD (pre-dispatch parent (loc ...) E)] [PDef bool] [SP bool] [SI bool] ; Dispatch types: ; event, curr node/null, phase, prevent default?, path, pending listeners, ; stack dispatch executes listener steps [D (dispatch E parent P PDef SP SI (loc ...) (L ...) L)] ; dispatch-collect looks for listeners [DC (dispatch-collect E parent P PDef SP SI (loc ...))] ; dispatch-next determines whether to visit a next node, to jump ; to the default action, or to terminate [DN (dispatch-next E parent P PDef SP SI (loc ...) (L ...))] ; dispatch-default executes the default action, unless prevented ; event, defaultPrevented, target loc [DD (dispatch-default E PDef loc)] ; dispatch-stupid handles the degenerate case of a single-node path [DS (dispatch-stupid loc E)] ; Listener steps [S skip (return bool) (seq S S) stop-prop stop-immediate prevent-default mutate (debug-print string) (addEventListener loc string bool loc) (removeEventListener loc string bool loc) (setEventHandler loc string S) (removeEventHandler loc string) (if-phase P S S) (if-curTarget loc S S) PD D DC DN DD DS] ; Contexts [DispCtx hole (if-phase DispCtx S S) (if-curTarget DispCtx S S) (seq DispCtx S)] [LCtx (listener bool Ctx) ;does there need to be a bool flag here? (handler Ctx)] [Ctx hole (seq Ctx S) (dispatch E parent P PDef SP SI (loc ...) (L ...) LCtx)] ; Machine state [N-store ((loc_!_n N) ... (loc_!_s S) ...)] [Log (string ...)] [M (state S N-store Log)]) (define-metafunction DOM ; NOTE: We're deferring looking up the handler until later, per the event handler processing algorithm [(lookup-listeners ((handler S) HL_wanted ...) ((loc_a S_a) ...)) ,(cons (term (gethandler)) (term (lookup-listeners (HL_wanted ...) ((loc_a S_a) ...))))] [(lookup-listeners ((nullhandler) HL_wanted ...) ((loc_a S_a) ...)) ,(cons (term (gethandler)) (term (lookup-listeners (HL_wanted ...) ((loc_a S_a) ...))))] [(lookup-listeners ((listener bool loc_listener) HL_wanted ...) ((loc_a S_a) ... (loc_listener S_listener) (loc_b S_b) ...)) ,(cons (term (listener bool S_listener)) (term (lookup-listeners (HL_wanted ...) ((loc_a S_a) ... (loc_listener S_listener) (loc_b S_b) ...))))] [(lookup-listeners () ((loc S) ...)) ()]) ; addEventListener ; 4.3 - EventTargetInterface ; Registers an event listener, depending on the useCapture parameter, on the ; capture phase of the DOM event flow or its target and bubbling phases. (define-metafunction DOM [(addListenerHelper ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ...)) (TP_b (HL_b ...)) ...) string_type P bool_useCapture loc_listener) ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ... (listener bool_useCapture loc_listener))) (TP_b (HL_b ...)) ...)] ;when (string_type P) is present [(addListenerHelper ((TP_a (HL_a ...)) ...) string_type P bool_useCapture loc_listener) ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_useCapture loc_listener))))]) ;when (string_type P) is absent (define-metafunction DOM [(listenerPresent ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ... (listener bool_useCapture loc) HL_q ...)) (TP_b (HL_b ...)) ...) string_type P bool_useCapture loc) #t] [(listenerPresent LS string P bool_useCapture loc) #f]) (define-metafunction DOM [(addListener LS string_type bool_useCapture loc_listener) ; From spec of addEventListener, sec 4.3 para 3 ; when the listener is already present, do nothing ,(let ([outerPhase (if (term bool_useCapture) (term capture) (term bubble))]) (if (term (listenerPresent LS string_type ,outerPhase bool_useCapture loc_listener)) (term LS) (term (addListenerHelper (addListenerHelper LS string_type target bool_useCapture loc_listener) string_type ,outerPhase bool_useCapture loc_listener))))]) ; removeEventListener ; 4.3 - EventTargetInterface ; Removes an event listener. Calling removeEventListener with arguments which ; do not identify any currently registered EventListener on the EventTarget has ; no effect. (define-metafunction DOM [(removeListenerHelper ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ... (listener bool_useCapture loc_listener) HL_q ...)) (TP_b (HL_b ...)) ...) string_type P bool_useCapture loc_listener) ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ... HL_q ...)) (TP_b (HL_b ...)) ...)] ;when (string_type P) is present [(removeListenerHelper ((TP_a (HL_a ...)) ...) string_type P bool_useCapture loc_listener) ((TP_a (HL_a ...)) ...)]) ;when (string_type P) is already absent (define-metafunction DOM [(removeListener LS string_type bool_useCapture loc_listener) (removeListenerHelper (removeListenerHelper LS string_type target bool_useCapture loc_listener) string_type ,(if (term bool_useCapture) (term capture) (term bubble)) bool_useCapture loc_listener)]) ; HTML5 Specification, Section 6.1.6.1 - Event handlers (define-metafunction DOM [(setHandlerHelper ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_p loc_p) ... (handler S_ignore) (listener bool_q loc_q) ...)) (TP_b (HL_b ...)) ...) string_type P S_handler) ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_p loc_p) ... (handler S_handler) (listener bool_q loc_q) ...)) (TP_b (HL_b ...)) ...)] ;if a handler was present for this (type, phase) pair, overwrite it [(setHandlerHelper ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_p loc_p) ... (nullhandler) (listener bool_q loc_q) ...)) (TP_b (HL_b ...)) ...) string_type P S_handler) ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_p loc_p) ... (handler S_handler) (listener bool_q loc_q) ...)) (TP_b (HL_b ...)) ...)] ;if a handler was once present for this (type, phase) pair, overwrite it [(setHandlerHelper ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ...)) (TP_b (HL_b ...)) ...) string_type P S_handler) ((TP_a (HL_a ...)) ... ((string_type P) (HL_p ... (handler S_handler) )) (TP_b (HL_b ...)) ...)] ;if a handler was missing for this (type, phase) pair, add it [(setHandlerHelper ((TP_a (HL_a ...)) ...) string_type P S_handler) ((TP_a (HL_a ...)) ... ((string_type P) ((handler S_handler))))] ) ; if nothing exists for this (type, phase) pair, add it (define-metafunction DOM [(setHandler LS string_type S_handler) (setHandlerHelper (setHandlerHelper LS string_type target S_handler) string_type bubble S_handler)]) (define-metafunction DOM [(removeHandlerHelper ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_p loc_p) ... (handler S_ignore) (listener bool_q loc_q) ...)) (TP_b (HL_b ...)) ...) string_type P) ((TP_a (HL_a ...)) ... ((string_type P) ((listener bool_p loc_p) ... (nullhandler) (listener bool_q loc_q) ...)) (TP_b (HL_b ...)) ...)] [(removeHandlerHelper LS string_type P) LS]) (define-metafunction DOM [(removeHandler LS string_type) (removeHandlerHelper (removeHandlerHelper LS string_type target) string_type bubble)]) ; getDefaultAction ; See 5.1.1 - List of DOM3 Event Types ;(define-metafunction DOM ; [(getDefaultAction (event "abort" #f #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "blur" #f #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "click" #t #t Trusted Meta) loc) ; (pre-dispatch loc () (event "DOMActivate" #t #t #f (("type" "click") ; ("fromscript" #f))))] ; ; For trusted compositionstart event, return default action... ; [(getDefaultAction (event "compositionstart" #t #t #t Meta) loc) ; (debug-print "launching text composition system...BEEP BEEP BOOP...")] ; ; ... for untrusted composition start event, do nothing ; [(getDefaultAction (event "compositionstart" #t #t #f Meta) loc) skip] ; [(getDefaultAction (event "compositionupdate" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "compositionend" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "dblclick" #t #f Trusted Meta) loc) skip] ; ; TODO: handle activation behavior/activation trigger ; [(getDefaultAction (event "DOMActivate" ; #t #t ; #f ; (("type" "click") ("fromscript" #f)) loc)) ; (debug-print "DOMActivate from click, not not from script")] ; [(getDefaultAction (event "DOMActivate" ; #t #t ; #f ; (("type" "click") ("fromscript" #t)) loc)) ; (debug-print "DOMActivate from click, from script")] ; [(getDefaultAction (event "DOMActivate" ; #t #t ; #f ; Meta) loc) ; (debug-print "DOMActivate from non-click")] ; [(getDefaultAction (event "DOMAttributeNameChanged" #t #f Trusted Meta) loc) ; skip] ; [(getDefaultAction (event "DOMAttrModified" #t #f Trusted Meta) loc) ; skip] ; [(getDefaultAction (event "DOMCharacterDataModified" #t #f Trusted Meta) loc) ; skip] ; [(getDefaultAction (event "DOMElementNameChanged" #t #f Trusted Meta) loc) ; skip] ; [(getDefaultAction (event "DOMFocusIn" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "DOMFocusOut" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "DOMNodeInserted" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "DOMNodeInsertedIntoDocument" #t #f Trusted Meta) ; loc) skip] ; [(getDefaultAction (event "DOMNodeRemoved" #t #f Trusted Meta) ; loc) skip] ; [(getDefaultAction (event "DOMNodeRemovedFromDocument" #t #f Trusted Meta) ; loc) skip] ; [(getDefaultAction (event "DOMSubtreeModified" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "focus" #f #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "focusin" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "focusout" #t #f Trusted Meta) loc) skip] ; ; TODO: handle keydown possibilities ; ; For trusted keydown event, return default action... ; [(getDefaultAction (event "keydown" ; #t #t #t ; (name Meta ; (("char" string_char) ; ("key" string_key) ; ("location" string_location) ; ("altKey" bool_alt) ; ("shiftKey" bool_shift) ; ("ctrlKey" bool_ctrl) ; ("metaKey" bool_meta) ; ("repeat" bool_repeat) ; ("locale" string_locale)))) loc) ; ,(handle-keydown (term Meta))] ; ; ... for untrusted, do nothing ; [(getDefaultAction (event "keydown" #t #t #f Meta) loc) skip] ; ; TODO: handle keypress possibilities ; ; For trusted keypress event, return default action ... ; [(getDefaultAction (event "keypress" ; #t #t #t ; (name Meta ; (("char" string_char) ; ("key" string_key) ; ("location" string_location) ; ("altKey" bool_alt) ; ("shiftKey" bool_shift) ; ("ctrlKey" bool_ctrl) ; ("metaKey" bool_meta) ; ("repeat" bool_repeat) ; ("locale" string_locale)))) loc) ; ,(handle-keypress (term Meta))] ; ; ... for untrusted, do nothing ; [(getDefaultAction (event "keypress" #t #t #f Meta) loc) skip] ; [(getDefaultAction (event "keyup" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "mousedown" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "mouseenter" #f #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "mouseleave" #f #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "mousemove" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "mouseout" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "mouseover" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "mouseup" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "resize" #f #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "select" #t #f Trusted Meta) loc) skip] ; [(getDefaultAction (event "textinput" #t #t Trusted Meta) loc) skip] ; [(getDefaultAction (event "unload" #f #f Trusted Meta) loc) skip]) (define (handle-keydown meta) (displayln "in handle-keydown!")) (define (handle-keypress meta) (displayln "in handle-keypress!")) (define DOM-reduce (reduction-relation DOM ; Building path in pre-dispatch ; 3.1 - Event dispatch and DOM event flow ; The propagation path must be an ordered list of event targets through ; which the event object must pass. For tree-based DOM implementations, the ; propagation path must be reflect the hierarchical tree structure of the ; document. The last item in the list must be the proximal event target; ; the preceding items in the list are referred to as the target's ancestors, ; and the immediately preceding item as the target's parent. (--> (state (in-hole Ctx (pre-dispatch loc_current (loc ...) E)) ((loc_b N_b) ... (loc_current (node string LS (loc_children ...) parent)) (loc_a N_a) ... (loc_c S_c) ...) Log) (state (in-hole Ctx (pre-dispatch parent (loc_current loc ...) E)) ((loc_b N_b) ... (loc_current (node string LS (loc_children ...) parent)) (loc_a N_a) ... (loc_c S_c) ...) Log) pd-build-path) ; Path building complete, transition to dispatch (--> (state (in-hole Ctx (pre-dispatch null (loc_first loc ...) E)) N-store Log) (state (in-hole Ctx (dispatch-collect E loc_first capture #f #f #f (loc_first loc ...))) N-store Log) pd-to-dispatch) ; Single-node path degenerate case (--> (state (in-hole Ctx (pre-dispatch null (loc) E)) N-store Log) (state (in-hole Ctx (dispatch-stupid loc E)) N-store Log) dont-do-this) ; done with current listener, determine next listener to run (if any) ; 3.1 - Event dispatch & DOM event flow ; ... the implementation must process all candidate event listeners in order ; and trigger each listener if all the following conditions are met: ; - The event object's immediate propagation has not been stopped. ; - The listener has been registered for this event phase. ; - The listener has been registered for this event type. (--> (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc_child ...) (L ...) (listener bool_useCapture skip))) N-store Log) (state (in-hole Ctx (dispatch-next E parent P PDef SP SI (loc_child ...) (L ...))) N-store Log) finished-listener) ; about to start handler, need to lookup what it is ; HTML5 specification, Section 6.1.6.1 - Event handler processing algorithm (--> (state (in-hole Ctx (dispatch (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef SP SI (loc_child ...) (L ...) (gethandler))) ((loc_a any_a) ... (loc_target (node string ((TP_a (HL_a ...)) ... ((T_event P) (HL_c ... (handler S_handler) HL_d ...)) (TP_b (HL_b ...)) ...) (loc_kids ...) parent)) (loc_b any_b) ...) Log) (state (in-hole Ctx (dispatch (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef SP SI (loc_child ...) (L ...) (handler S_handler))) ((loc_a any_a) ... (loc_target (node string ((TP_a (HL_a ...)) ... ((T_event P) (HL_c ... (handler S_handler) HL_d ...)) (TP_b (HL_b ...)) ...) (loc_kids ...) parent)) (loc_b any_b) ...) Log) gethandler-found-handler) (--> (state (in-hole Ctx (dispatch (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef SP SI (loc_child ...) (L ...) (gethandler))) ((loc_a any_a) ... (loc_target (node string ((TP_a (HL_a ...)) ... ((T_event P) (HL_c ... (nullhandler) HL_d ...)) (TP_b (HL_b ...)) ...) (loc_kids ...) parent)) (loc_b any_b) ...) Log) (state (in-hole Ctx (dispatch-next (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef SP SI (loc_child ...) (L ...))) ((loc_a any_a) ... (loc_target (node string ((TP_a (HL_a ...)) ... ((T_event P) (HL_c ... (nullhandler) HL_d ...)) (TP_b (HL_b ...)) ...) (loc_kids ...) parent)) (loc_b any_b) ...) Log) gethandler-no-handler) ; done with current handler, determine what steps to take ; HTML5 Specification, Section 6.1.6.1 - Event handlers ; http://www.w3.org/TR/html5/webappapis.html#event-handler-attributes (--> (state (in-hole Ctx (dispatch (event T_event Bubbles Cancels Trusted Meta loc_default) parent P PDef SP SI (loc_child ...) (L ...) (handler (in-hole DispCtx (return bool))))) N-store Log) (state (in-hole Ctx (dispatch (event T_event Bubbles Cancels Trusted Meta loc_default) parent P PDef SP SI (loc_child ...) (L ...) (listener #f ,(if (equal? (term bool) (equal? (term T_event) "mouseover")) (term prevent-default) (term skip))))) N-store Log) return-from-handler) ; when we finish a handler, this rule transmutes it into the exit from a listener (--> (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc_child ...) (L ...) (handler skip))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc_child ...) (L ...) (handler (return #f)))) N-store Log) finished-handler) ; stop-immediate-prop called, abort dispatch and jump to default action ; 3.1 - Event dispatch and DOM event flow ; ... the implementation must process all candidate event listeners in order ; and trigger each listener if all the following conditions are met: ; ... ; - The event object's immediate propagation has not been stopped. ; ... (--> (state (in-hole Ctx (dispatch-next E parent P PDef SP #t (loc_child ... loc_target) (L ...))) N-store Log) (state (in-hole Ctx (dispatch-default E PDef loc_target)) N-store Log) stop-immediate-called) ; stop-propagation called, finish current node, and then abort dispatch and ; jump to default action ; 3.1 - Event dispatch and DOM event flow ; ... Implementations must let event objects accomplish an event phase by ; applying the following steps while there are pending event targets in the ; partial propagation path for this phase and the event object's propagation ; has not been stopped through Event.stopPropagation() ... (--> (state (in-hole Ctx (dispatch-next E parent P PDef #t #f (loc_child ...) (L L_rest ...))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef #t #f (loc_child ...) (L_rest ...) L)) N-store Log) stop-prop-called-more-to-do) (--> (state (in-hole Ctx (dispatch-next E parent P PDef #t #f (loc_child ... loc_target) ())) N-store Log) (state (in-hole Ctx (dispatch-default E PDef loc_target)) N-store Log) stop-prop-called-done-with-node) ; neither stop-prop nor stop-imm-prop called, do next listener on current node (--> (state (in-hole Ctx (dispatch-next E parent P PDef #f #f (loc_child ...) (L L_rest ...))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef #f #f (loc_child ...) (L_rest ...) L)) N-store Log) more-to-do) ; neither stop-prop nor stop-imm-prop called, no listeners left on current node, ; rules for capture, target, bubble ; capture->capture ; 3.1 - Event dispatch & DOM event flow ; The capture phase: the event object must propagate through the ; target's ancestors from the defaultView to the target's parent. This phase ; is also known as the capturing phase. Event listeners registered for this ; phase must handle the event before it reaches its target. (--> (state (in-hole Ctx (dispatch-next E loc_parent capture PDef #f #f (loc_a ... loc_parent loc_child loc_grand loc_b ...) ())) N-store Log) (state (in-hole Ctx (dispatch-collect E loc_child capture PDef #f #f (loc_a ... loc_parent loc_child loc_grand loc_b ...))) N-store Log) capture-to-capture-collect) ; capture->target ; 3.1 - Event dispatch & DOM event flow ; The target phase: the event object must arrive at the event object's ; proximal event target. This phase is also known as the at-target phase. ; Event listeners registered for this phase must handle the event once it ; has reached its target. (--> (state (in-hole Ctx (dispatch-next E loc_parent capture PDef #f #f (loc_a ... loc_parent loc_child) ())) N-store Log) (state (in-hole Ctx (dispatch-collect E loc_child target PDef #f #f (loc_a ... loc_parent loc_child))) N-store Log) capture-to-target-collect) ; target->bubble & event bubbles (--> (state (in-hole Ctx (dispatch-next (event T_event #t Cancels Trusted Meta loc_default) loc_child target PDef #f #f (loc_a ... loc_parent loc_child) ())) N-store Log) (state (in-hole Ctx (dispatch-collect (event T_event #t Cancels Trusted Meta loc_default) loc_parent bubble PDef #f #f (loc_a ... loc_parent loc_child))) N-store Log) target-to-bubble-collect) ; target->default & event doesn't bubble ; 3.1 - Event dispatch & DOM event flow ; ... If the event type indicates that the event must not bubble, the event ; object must halt after completion of this phase.... (--> (state (in-hole Ctx (dispatch-next (event T_event #f Cancels Trusted Meta loc_default) loc_child target PDef #f #f (loc_a ... loc_child) ())) N-store Log) (state (in-hole Ctx (dispatch-default (event T_event #f Cancels Trusted Meta loc_default) PDef loc_child)) N-store Log) target-to-default) ; bubble->bubble ; 3.1 - Event dispatch & DOM event flow ; The bubble phase: the event object propagates through the target's ; ancestors in reverse order, starting with the target's parent and ending ; with the defaultView. This phase is also known as the bubbling phase. ; Event listeners registered for this phase must handle the event after it ; has reached its target. (--> (state (in-hole Ctx (dispatch-next E loc_child bubble PDef #f #f (loc_a ... loc_parent loc_child loc_b ...) ())) N-store Log) (state (in-hole Ctx (dispatch-collect E loc_parent bubble PDef #f #f (loc_a ... loc_parent loc_child loc_b ...))) N-store Log) bubble-to-bubble-collect) ; bubble->default (--> (state (in-hole Ctx (dispatch-next E loc_root bubble PDef #f #f (loc_root loc_b ... loc_target) ())) N-store Log) (state (in-hole Ctx (dispatch-default E PDef loc_target)) N-store Log) bubble-to-default) ; collecting listeners on current node, and listeners are found (--> (state (in-hole Ctx (dispatch-collect (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef #f #f (loc_a ... loc_target loc_b ...))) ((loc_c N_c) ... (loc_target (node string ((TP_a (HL_a ...)) ... ((T_event P) (HL_wanted ...)) (TP_b (HL_b ...)) ...) (loc_kids ...) parent)) (loc_d N_d) ... (loc_e S_e) ...) Log) (state (in-hole Ctx (dispatch-next (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef #f #f (loc_a ... loc_target loc_b ...) (lookup-listeners (HL_wanted ...) ((loc_e S_e) ...)))) ((loc_c N_c) ... (loc_target (node string ((TP_a (HL_a ...)) ... ((T_event P) (HL_wanted ...)) (TP_b (HL_b ...)) ...) (loc_kids ...) parent)) (loc_d N_d) ... (loc_e S_e) ...) Log) collect-found-listeners) ; collecting listeners on current node, and listeners are not found (--> (side-condition (state (in-hole Ctx (dispatch-collect (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef #f #f (loc_a ... loc_target loc_b ...))) ((loc_c N_c) ... (loc_target (node string ((TP_a (HL_a ...)) ...) (loc_kids ...) parent)) (loc_d N_d) ... (loc_e S_e) ...) Log) (not-in? (term T_event) (term P) (term (TP_a ...)))) (state (in-hole Ctx (dispatch-next (event T_event Bubbles Cancels Trusted Meta loc_default) loc_target P PDef #f #f (loc_a ... loc_target loc_b ...) ())) ((loc_c N_c) ... (loc_target (node string ((TP_a (HL_a ...)) ...) (loc_kids ...) parent)) (loc_d N_d) ... (loc_e S_e) ...) Log) collect-found-no-listeners) ; seq-skip (--> (state (in-hole Ctx (seq skip S)) N-store Log) (state (in-hole Ctx S) N-store Log) seq-skip) ; addEventListener ; 4.3 - EventTarget interface ; Registers an event listener, depending on the useCapture parameter, on the ; capture phase of the DOM event flow or its target and bubbling phases. (--> (state (in-hole Ctx (addEventListener loc_target string_type bool loc_listener)) ((loc_a N_a) ... (loc_target (node string_name LS (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ... (loc_listener S_listener) (loc_d S_d) ...) Log) (state (in-hole Ctx skip) ((loc_a N_a) ... (loc_target (node string_name (addListener LS string_type bool loc_listener) (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ... (loc_listener S_listener) (loc_d S_d) ...) Log) do-addEventListener) ; removeEventListener ; 4.3 - EventTarget interface ; Removes an event listener. Calling removeEventListener with arguments ; which do not identify any currently registered EventListener on the ; EventTarget has no effect. (--> (state (in-hole Ctx (removeEventListener loc_target string_type bool loc_listener)) ((loc_a N_a) ... (loc_target (node string_name LS (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ... (loc_listener S_listener) (loc_d S_d) ...) Log) (state (in-hole Ctx skip) ((loc_a N_a) ... (loc_target (node string_name (removeListener LS string_type bool loc_listener) (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ... (loc_listener S_listener) (loc_d S_d) ...) Log) do-removeEventListener) ; setEventHandler (--> (state (in-hole Ctx (setEventHandler loc_target string_type S_listener)) ((loc_a N_a) ... (loc_target (node string_name LS (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ...) Log) (state (in-hole Ctx skip) ((loc_a N_a) ... (loc_target (node string_name (setHandler LS string_type S_listener) (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ...) Log) do-setEventHandler) ; setEventHandler (--> (state (in-hole Ctx (removeEventHandler loc_target string_type)) ((loc_a N_a) ... (loc_target (node string_name LS (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ...) Log) (state (in-hole Ctx skip) ((loc_a N_a) ... (loc_target (node string_name (removeHandler LS string_type) (loc_kids ...) parent_node)) (loc_b N_b) ... (loc_c S_c) ...) Log) do-removeEventHandler) ; debug-print (--> (state (in-hole Ctx (debug-print string_new)) N-store (string_log ...)) (state (in-hole Ctx skip) N-store (string_log ... string_new)) debug-print) ; if-phase (--> (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx (if-phase P_check S_true S_false))))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx ,(if (equal? (term P) (term P_check)) (term S_true) (term S_false)))))) N-store Log) do-if-phase) ; if-curTarget (--> (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx (if-curTarget loc_check S_true S_false))))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx ,(if (equal? (term parent) (term loc_check)) (term S_true) (term S_false)))))) N-store Log) do-if-curTarget) ; stopPropagation ; 4.1 - Event interface ; Prevents other event listeners from being triggered but its effect must be ; deferred until all event listeners attached on the Event.currentTarget ; have been triggered. Once it has been called, further calls to this method ; have no additional effect. (--> (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx stop-prop)))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef #t SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx skip)))) N-store Log) do-stop-prop) ; stopImmediatePropagation ; 4.1 - Event interface ; Prevents other event listeners from being triggered and, unlike ; Event.stopPropagation() its effect must be immediate . Once it has been ; called, further calls to this method have no additional effect. (--> (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx stop-immediate)))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef #t #t (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx skip)))) N-store Log) do-stop-immediate) ; preventDefault ; 4.1 - Event interface ; When this method is invoked, the event must be canceled, meaning any ; default actions normally taken by the implementation as a result of the ; event must not occur (see also Default actions and cancelable events). ; Default actions which occur prior to the event's dispatch (see Default ; actions and cancelable events) are reverted. Calling this method for a ; non-cancelable event must have no effect. If an event has more than one ; default action, each cancelable default action must be canceled. (--> (state (in-hole Ctx (dispatch (name E (event T Bubbles #t Trusted Meta loc_default)) parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx prevent-default)))) N-store Log) (state (in-hole Ctx (dispatch E parent P #t SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx skip)))) N-store Log) do-prevent-default-cancelable) (--> (state (in-hole Ctx (dispatch (name E (event T Bubbles #f Trusted Meta loc_default)) parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx prevent-default)))) N-store Log) (state (in-hole Ctx (dispatch E parent P PDef SP SI (loc ...) (L ...) (in-hole LCtx (in-hole DispCtx skip)))) N-store Log) do-prevent-default-not-cancelable) ; 3.2 - Default actions and cancelable events ; A default action is an optional supplementary behavior that an ; implementation must perform in combination with the dispatch of the event ; object. Each event type definition, and each specification, defines the ; default action for that event type, if it has one. An instance of an event ; may have more than one default action under some circumstances, such as ; when associated with an activation trigger. A default action may be ; cancelled through the invocation of the Event.preventDefault() method. ; dispatch-default-prevented (--> (state (in-hole Ctx (dispatch-default E_inner #t loc_target)) N-store Log) (state (in-hole Ctx skip) ;(debug-print "default-prevented")) N-store Log) dispatch-default-prevented) ; dispatch-default-not-prevented (--> (state (in-hole Ctx (dispatch-default (name E_inner (event T Bubbles Cancels #t Meta loc_default)) #f loc_target)) ((loc_a N_a) ... (loc_b S_b) ... (loc_default S_default) (loc_c S_c) ...) Log) (state (in-hole Ctx S_default) ((loc_a N_a) ... (loc_b S_b) ... (loc_default S_default) (loc_c S_c) ...) Log) dispatch-not-default-prevented) ; untrusted non-click non-DOMActivate event -> shouldn't do default action (--> (state (in-hole Ctx (dispatch-default (name E_inner (side-condition (event T Bubbles Cancels #f Meta loc_default) (let ([event-type (term T)]) (and (not (equal? event-type "click")) (not (equal? event-type "DOMActivate")))))) #f loc_target)) N-store Log) (state (in-hole Ctx (debug-print "untrusted event, default action skipped")) N-store Log) untrusted-skip-default) ; click or DOMActivate events should do default action if they were ; generated from an activation trigger ; See 3.4, paragraph 2 (--> (state (in-hole Ctx (dispatch-default (name E_inner (side-condition (event T Bubbles Cancels #f ((string_b any_b) ... ("fromscript" #f) (string_a any_a) ...) loc_default) (let ([event-type (term T)]) (or (equal? event-type "click") (equal? event-type "DOMActivate"))))) #f loc_target)) ((loc_a N_a) ... (loc_b S_b) ... (loc_default S_default) (loc_c S_c) ...) Log) (state (in-hole Ctx S_default) ((loc_a N_a) ... (loc_b S_b) ... (loc_default S_default) (loc_c S_c) ...) Log) do-click-domactivate-default) (--> (state (in-hole Ctx (dispatch-default (name E_inner (side-condition (event T Bubbles Cancels #f ((string_b any_b) ... ("fromscript" #t) (string_a any_a) ...) loc_default) (let ([event-type (term T)]) (or (equal? event-type "click") (equal? event-type "DOMActivate"))))) #f loc_target)) ((loc_a N_a) ... (loc_b S_b) ... (loc_default S_default) (loc_c S_c) ...) Log) (state (in-hole Ctx (debug-print "click or DOMActivate from script, skipped DA")) ((loc_a N_a) ... (loc_b S_b) ... (loc_default S_default) (loc_c S_c) ...) Log) skip-click-domactivate-default) (--> (state (in-hole Ctx mutate) N-store Log) (state (in-hole Ctx skip) N-store Log) skip-mutate) ))