Anubis / Xlib

Commit e45144c27f2777f307927e44452742dc1964a5e6

Authored by totoro
1 parent 3c4d7fe5

add all HTML5 event

Showing 1 changed file with 155 additions and 34 deletions   Show diff stats
Inline Side-by-side
web/CXM_making_a_web_site.anubis
  Show/Hide comments   View file @e45144c
@@ -934,25 +934,86 @@ public define Printable_tree [InitialValue x . Printable_tree y] = str_pt(x.valu @@ -934,25 +934,86 @@ public define Printable_tree [InitialValue x . Printable_tree y] = str_pt(x.valu
934 934
935 935
936 public type HtmlEvents: 936 public type HtmlEvents:
  937 + // Window Event Attributes
  938 + onafterprint, //HTML5 Script to be run after the document is printed
  939 + onbeforeprint, //HTML5 Script to be run before the document is printed
  940 + onbeforeunload, //HTML5 Script to be run when the document is about to be unloaded
  941 + onerror, //HTML5 Script to be run when an error occurs
  942 + onhashchange, //HTML5 Script to be run when there has been changes to the anchor part of the a URL
  943 + onload, // Fires after the page is finished loading
  944 + onmessage, //HTML5 Script to be run when the message is triggered
  945 + onoffline, //HTML5 Script to be run when the browser starts to work offline
  946 + ononline, //HTML5 Script to be run when the browser starts to work online
  947 + onpagehide, //HTML5 Script to be run when a user navigates away from a page
  948 + onpageshow, //HTML5 Script to be run when a user navigates to a page
  949 + onpopstate, //HTML5 Script to be run when the window's history changes
  950 + onresize, //HTML5 Fires when the browser window is resized
  951 + onstorage, //HTML5 Script to be run when a Web Storage area is updated
  952 + onunload, // Fires once a page has unloaded (or the browser window has been closed)
937 // Form element events 953 // Form element events
938 - onchange,  
939 - onsubmit,  
940 - onreset,  
941 - onselect,  
942 - onblur,  
943 - onfocus, 954 + onblur, // Fires the moment that the element loses focus
  955 + onchange, // Fires the moment when the value of the element is changed
  956 + oncontextmenu, //HTML5 Script to be run when a context menu is triggered
  957 + onfocus, // Fires the moment when the element gets focus
  958 + oninput, //HTML5 Script to be run when an element gets user input
  959 + oninvalid, //HTML5 Script to be run when an element is invalid
  960 + onreset, // Fires when the Reset button in a form is clicked
  961 + onsearch, // Fires when the user writes something in a search field (for <input="search">)
  962 + onselect, // Fires after some text has been selected in an element
  963 + onsubmit, // Fires when a form is submitted
944 // Keyboard events (Not valid in base, bdo, br, frame, frameset, head, html, iframe, meta, param, script, style, and title elements.) 964 // Keyboard events (Not valid in base, bdo, br, frame, frameset, head, html, iframe, meta, param, script, style, and title elements.)
945 - onkeydown,  
946 - onkeypress,  
947 - onkeyup, 965 + onkeydown, // Fires when a user is pressing a key
  966 + onkeypress, // Fires when a user presses a key
  967 + onkeyup, // Fires when a user releases a key
948 // Mouse events (Not valid in base, bdo, br, frame, frameset, head, html, iframe, meta, param, script, style, and title elements.) 968 // Mouse events (Not valid in base, bdo, br, frame, frameset, head, html, iframe, meta, param, script, style, and title elements.)
949 - onclick,  
950 - ondblclick,  
951 - onmousedown,  
952 - onmousemove,  
953 - onmouseout,  
954 - onmouseover,  
955 - onmouseup. 969 + onclick, // Fires on a mouse click on the element
  970 + ondblclick, // Fires on a mouse double-click on the element
  971 + onmousedown, // Fires when a mouse button is pressed down on an element
  972 + onmousemove, // Fires when the mouse pointer is moving while it is over an element
  973 + onmouseout, // Fires when the mouse pointer moves out of an element
  974 + onmouseover, // Fires when the mouse pointer moves over an element
  975 + onmouseup, // Fires when a mouse button is released over an element
  976 + onwheel, //HTML5 Fires when the mouse wheel rolls up or down over an element
  977 + //Drag Events
  978 + ondrag, //HMTL5 Script to be run when an element is dragged
  979 + ondragend, //HTML5 Script to be run at the end of a drag operation
  980 + ondragenter, //HTML5 Script to be run when an element has been dragged to a valid drop target
  981 + ondragleave, //HTML5 Script to be run when an element leaves a valid drop target
  982 + ondragover, //HTML5 Script to be run when an element is being dragged over a valid drop target
  983 + ondragstart, //HTML5 Script to be run at the start of a drag operation
  984 + ondrop, //HTML5 Script to be run when dragged element is being dropped
  985 + onscroll, //HTML5 Script to be run when an element's scrollbar is being scrolled
  986 + //Clipboard Events
  987 + oncopy, //HTML5 Fires when the user copies the content of an element
  988 + oncut, //HTML5 Fires when the user cuts the content of an element
  989 + onpaste, //HTML5 Fires when the user pastes some content in an element
  990 + //Media Events
  991 + onabort, //HTML5 Script to be run on abort
  992 + oncanplay, //HTML5 Script to be run when a file is ready to start playing (when it has buffered enough to begin)
  993 + oncanplaythrough, //HTML5 Script to be run when a file can be played all the way to the end without pausing for buffering
  994 + oncuechange, //HTML5 Script to be run when the cue changes in a <track> element
  995 + ondurationchange, //HTML5 Script to be run when the length of the media changes
  996 + onemptied, //HTML5 Script to be run when something bad happens and the file is suddenly unavailable (like unexpectedly disconnects)
  997 + onended, //HTML5 Script to be run when the media has reach the end (a useful event for messages like "thanks for listening")
  998 + onerror, //HTML5 Script to be run when an error occurs when the file is being loaded
  999 + onloadeddata, //HTML5 Script to be run when media data is loaded
  1000 + onloadedmetadata, //HTML5 Script to be run when meta data (like dimensions and duration) are loaded
  1001 + onloadstart, //HTML5 Script to be run just as the file begins to load before anything is actually loaded
  1002 + onpause, //HTML5 Script to be run when the media is paused either by the user or programmatically
  1003 + onplay, //HTML5 Script to be run when the media is ready to start playing
  1004 + onplaying, //HTML5 Script to be run when the media actually has started playing
  1005 + onprogress, //HTML5 Script to be run when the browser is in the process of getting the media data
  1006 + onratechange, //HTML5 Script to be run each time the playback rate changes (like when a user switches to a slow motion or fast forward mode)
  1007 + onseeked, //HTML5 Script to be run when the seeking attribute is set to false indicating that seeking has ended
  1008 + onseeking, //HTML5 Script to be run when the seeking attribute is set to true indicating that seeking is active
  1009 + onstalled, //HTML5 Script to be run when the browser is unable to fetch the media data for whatever reason
  1010 + onsuspend, //HTML5 Script to be run when fetching the media data is stopped before it is completely loaded for whatever reason
  1011 + ontimeupdate, //HTML5 Script to be run when the playing position has changed (like when the user fast forwards to a different point in the media)
  1012 + onvolumechange, //HTML5 Script to be run each time the volume is changed which (includes setting the volume to "mute")
  1013 + onwaiting, //HTML5 Script to be run when the media has paused but is expected to resume (like when the media pauses to buffer more data)
  1014 + //Misc Events
  1015 + onshow, //HTML5 Fires when a <menu> element is shown as a context menu
  1016 + ontoggle. //HTML5 Fires when the user opens or closes the <details> element
956 1017
957 public type CoreAttrs: 1018 public type CoreAttrs:
958 id (String), 1019 id (String),
@@ -1031,25 +1092,85 @@ define String event_name @@ -1031,25 +1092,85 @@ define String event_name
1031 ) = 1092 ) =
1032 if e is 1093 if e is
1033 { 1094 {
  1095 + onafterprint then "onafterprint", //HTML5 Script to be run after the document is printed
  1096 + onbeforeprint then "onbeforeprint", //HTML5 Script to be run before the document is printed
  1097 + onbeforeunload then "onbeforeunload", //HTML5 Script to be run when the document is about to be unloaded
  1098 + onerror then "onerror", //HTML5 Script to be run when an error occurs
  1099 + onhashchange then "onhashchange", //HTML5 Script to be run when there has been changes to the anchor part of the a URL
  1100 + onload then "onload", // Fires after the page is finished loading
  1101 + onmessage then "onmessage", //HTML5 Script to be run when the message is triggered
  1102 + onoffline then "onoffline", //HTML5 Script to be run when the browser starts to work offline
  1103 + ononline then "ononline", //HTML5 Script to be run when the browser starts to work online
  1104 + onpagehide then "onpagehide", //HTML5 Script to be run when a user navigates away from a page
  1105 + onpageshow then "onpageshow", //HTML5 Script to be run when a user navigates to a page
  1106 + onpopstate then "onpopstate", //HTML5 Script to be run when the window's history changes
  1107 + onresize then "onresize", //HTML5 Fires when the browser window is resized
  1108 + onstorage then "onstorage", //HTML5 Script to be run when a Web Storage area is updated
  1109 + onunload then "onunload", // Fires once a page has unloaded (or the browser window has been closed)
1034 // Form element events 1110 // Form element events
1035 - onchange then "onchange",  
1036 - onsubmit then "onsubmit",  
1037 - onreset then "onreset",  
1038 - onselect then "onselect",  
1039 - onblur then "onblur",  
1040 - onfocus then "onfocus",  
1041 - // Keyboard events  
1042 - onkeydown then "onkeydown",  
1043 - onkeypress then "onkeypress",  
1044 - onkeyup then "onkeyup",  
1045 - // Mouse events  
1046 - onclick then "onclick",  
1047 - ondblclick then "ondblclick",  
1048 - onmousedown then "onmousedown",  
1049 - onmousemove then "onmousemove",  
1050 - onmouseout then "onmouseout",  
1051 - onmouseover then "onmouseover",  
1052 - onmouseup then "onmouseup" 1111 + onblur then "onblur", // Fires the moment that the element loses focus
  1112 + onchange then "onchange", // Fires the moment when the value of the element is changed
  1113 + oncontextmenu then "oncontextmenu", //HTML5 Script to be run when a context menu is triggered
  1114 + onfocus then "onfocus", // Fires the moment when the element gets focus
  1115 + oninput then "oninput", //HTML5 Script to be run when an element gets user input
  1116 + oninvalid then "oninvalid", //HTML5 Script to be run when an element is invalid
  1117 + onreset then "onreset", // Fires when the Reset button in a form is clicked
  1118 + onsearch then "onsearch", // Fires when the user writes something in a search field (for <input="search">)
  1119 + onselect then "onselect", // Fires after some text has been selected in an element
  1120 + onsubmit then "onsubmit", // Fires when a form is submitted
  1121 + // Keyboard events (Not valid in base, bdo, br, frame, frameset, head, html, iframe, meta, param, script, style, and title elements.)
  1122 + onkeydown then "onkeydown", // Fires when a user is pressing a key
  1123 + onkeypress then "onkeypress", // Fires when a user presses a key
  1124 + onkeyup then "onkeyup", // Fires when a user releases a key
  1125 + // Mouse events (Not valid in base, bdo, br, frame, frameset, head, html, iframe, meta, param, script, style, and title elements.)
  1126 + onclick then "onclick", // Fires on a mouse click on the element
  1127 + ondblclick then "ondblclick", // Fires on a mouse double-click on the element
  1128 + onmousedown then "onmousedown", // Fires when a mouse button is pressed down on an element
  1129 + onmousemove then "onmousemove", // Fires when the mouse pointer is moving while it is over an element
  1130 + onmouseout then "onmouseout", // Fires when the mouse pointer moves out of an element
  1131 + onmouseover then "onmouseover", // Fires when the mouse pointer moves over an element
  1132 + onmouseup then "onmouseup", // Fires when a mouse button is released over an element
  1133 + onwheel then "onwheel", //HTML5 Fires when the mouse wheel rolls up or down over an element
  1134 + //Drag Events
  1135 + ondrag then "ondrag", //HMTL5 Script to be run when an element is dragged
  1136 + ondragend then "ondragend", //HTML5 Script to be run at the end of a drag operation
  1137 + ondragenter then "ondragenter", //HTML5 Script to be run when an element has been dragged to a valid drop target
  1138 + ondragleave then "ondragleave", //HTML5 Script to be run when an element leaves a valid drop target
  1139 + ondragover then "ondragover", //HTML5 Script to be run when an element is being dragged over a valid drop target
  1140 + ondragstart then "ondragstart", //HTML5 Script to be run at the start of a drag operation
  1141 + ondrop then "ondrop", //HTML5 Script to be run when dragged element is being dropped
  1142 + onscroll then "onscroll", //HTML5 Script to be run when an element's scrollbar is being scrolled
  1143 + //Clipboard Events
  1144 + oncopy then "oncopy", //HTML5 Fires when the user copies the content of an element
  1145 + oncut then "oncut", //HTML5 Fires when the user cuts the content of an element
  1146 + onpaste then "onpaste", //HTML5 Fires when the user pastes some content in an element
  1147 + //Media Events
  1148 + onabort then "onabort", //HTML5 Script to be run on abort
  1149 + oncanplay then "oncanplay", //HTML5 Script to be run when a file is ready to start playing (when it has buffered enough to begin)
  1150 + oncanplaythrough then "oncanplaythrough", //HTML5 Script to be run when a file can be played all the way to the end without pausing for buffering
  1151 + oncuechange then "oncuechange", //HTML5 Script to be run when the cue changes in a <track> element
  1152 + ondurationchange then "ondurationchange", //HTML5 Script to be run when the length of the media changes
  1153 + onemptied then "onemptied", //HTML5 Script to be run when something bad happens and the file is suddenly unavailable (like unexpectedly disconnects)
  1154 + onended then "onended", //HTML5 Script to be run when the media has reach the end (a useful event for messages like "thanks for listening")
  1155 + onerror then "onerror", //HTML5 Script to be run when an error occurs when the file is being loaded
  1156 + onloadeddata then "onloadeddata", //HTML5 Script to be run when media data is loaded
  1157 + onloadedmetadata then "onloadedmetadata", //HTML5 Script to be run when meta data (like dimensions and duration) are loaded
  1158 + onloadstart then "onloadstart", //HTML5 Script to be run just as the file begins to load before anything is actually loaded
  1159 + onpause then "onpause", //HTML5 Script to be run when the media is paused either by the user or programmatically
  1160 + onplay then "onplay", //HTML5 Script to be run when the media is ready to start playing
  1161 + onplaying then "onplaying", //HTML5 Script to be run when the media actually has started playing
  1162 + onprogress then "onprogress", //HTML5 Script to be run when the browser is in the process of getting the media data
  1163 + onratechange then "onratechange", //HTML5 Script to be run each time the playback rate changes (like when a user switches to a slow motion or fast forward mode)
  1164 + onseeked then "onseeked", //HTML5 Script to be run when the seeking attribute is set to false indicating that seeking has ended
  1165 + onseeking then "onseeking", //HTML5 Script to be run when the seeking attribute is set to true indicating that seeking is active
  1166 + onstalled then "onstalled", //HTML5 Script to be run when the browser is unable to fetch the media data for whatever reason
  1167 + onsuspend then "onsuspend", //HTML5 Script to be run when fetching the media data is stopped before it is completely loaded for whatever reason
  1168 + ontimeupdate then "ontimeupdate", //HTML5 Script to be run when the playing position has changed (like when the user fast forwards to a different point in the media)
  1169 + onvolumechange then "onvolumechange", //HTML5 Script to be run each time the volume is changed which (includes setting the volume to "mute")
  1170 + onwaiting then "onwaiting", //HTML5 Script to be run when the media has paused but is expected to resume (like when the media pauses to buffer more data)
  1171 + //Misc Events
  1172 + onshow then "onshow", //HTML5 Fires when a <menu> element is shown as a context menu
  1173 + ontoggle then "ontoggle"
1053 }. 1174 }.
1054 1175
1055 public type Table_Option: 1176 public type Table_Option: