0 | module Web.Internal.UIEventsTypes
  1 |
  2 | import JS
  3 |
  4 | %default total
  5 |
  6 |
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          Interfaces
 10 | --------------------------------------------------------------------------------
 11 |
 12 | export data CompositionEvent : Type where [external]
 13 |
 14 | export
 15 | ToFFI CompositionEvent CompositionEvent where toFFI = id
 16 |
 17 | export
 18 | FromFFI CompositionEvent CompositionEvent where fromFFI = Just
 19 |
 20 | export
 21 | SafeCast CompositionEvent where
 22 |   safeCast = unsafeCastOnPrototypeName "CompositionEvent"
 23 |
 24 | export data FocusEvent : Type where [external]
 25 |
 26 | export
 27 | ToFFI FocusEvent FocusEvent where toFFI = id
 28 |
 29 | export
 30 | FromFFI FocusEvent FocusEvent where fromFFI = Just
 31 |
 32 | export
 33 | SafeCast FocusEvent where
 34 |   safeCast = unsafeCastOnPrototypeName "FocusEvent"
 35 |
 36 | export data InputEvent : Type where [external]
 37 |
 38 | export
 39 | ToFFI InputEvent InputEvent where toFFI = id
 40 |
 41 | export
 42 | FromFFI InputEvent InputEvent where fromFFI = Just
 43 |
 44 | export
 45 | SafeCast InputEvent where
 46 |   safeCast = unsafeCastOnPrototypeName "InputEvent"
 47 |
 48 | export data KeyboardEvent : Type where [external]
 49 |
 50 | export
 51 | ToFFI KeyboardEvent KeyboardEvent where toFFI = id
 52 |
 53 | export
 54 | FromFFI KeyboardEvent KeyboardEvent where fromFFI = Just
 55 |
 56 | export
 57 | SafeCast KeyboardEvent where
 58 |   safeCast = unsafeCastOnPrototypeName "KeyboardEvent"
 59 |
 60 | export data MouseEvent : Type where [external]
 61 |
 62 | export
 63 | ToFFI MouseEvent MouseEvent where toFFI = id
 64 |
 65 | export
 66 | FromFFI MouseEvent MouseEvent where fromFFI = Just
 67 |
 68 | export
 69 | SafeCast MouseEvent where
 70 |   safeCast = unsafeCastOnPrototypeName "MouseEvent"
 71 |
 72 | export data UIEvent : Type where [external]
 73 |
 74 | export
 75 | ToFFI UIEvent UIEvent where toFFI = id
 76 |
 77 | export
 78 | FromFFI UIEvent UIEvent where fromFFI = Just
 79 |
 80 | export
 81 | SafeCast UIEvent where
 82 |   safeCast = unsafeCastOnPrototypeName "UIEvent"
 83 |
 84 | export data WheelEvent : Type where [external]
 85 |
 86 | export
 87 | ToFFI WheelEvent WheelEvent where toFFI = id
 88 |
 89 | export
 90 | FromFFI WheelEvent WheelEvent where fromFFI = Just
 91 |
 92 | export
 93 | SafeCast WheelEvent where
 94 |   safeCast = unsafeCastOnPrototypeName "WheelEvent"
 95 |
 96 |
 97 | --------------------------------------------------------------------------------
 98 | --          Dictionaries
 99 | --------------------------------------------------------------------------------
100 |
101 | export data CompositionEventInit : Type where [external]
102 |
103 | export
104 | ToFFI CompositionEventInit CompositionEventInit where toFFI = id
105 |
106 | export
107 | FromFFI CompositionEventInit CompositionEventInit where fromFFI = Just
108 |
109 | export data EventModifierInit : Type where [external]
110 |
111 | export
112 | ToFFI EventModifierInit EventModifierInit where toFFI = id
113 |
114 | export
115 | FromFFI EventModifierInit EventModifierInit where fromFFI = Just
116 |
117 | export data FocusEventInit : Type where [external]
118 |
119 | export
120 | ToFFI FocusEventInit FocusEventInit where toFFI = id
121 |
122 | export
123 | FromFFI FocusEventInit FocusEventInit where fromFFI = Just
124 |
125 | export data InputEventInit : Type where [external]
126 |
127 | export
128 | ToFFI InputEventInit InputEventInit where toFFI = id
129 |
130 | export
131 | FromFFI InputEventInit InputEventInit where fromFFI = Just
132 |
133 | export data KeyboardEventInit : Type where [external]
134 |
135 | export
136 | ToFFI KeyboardEventInit KeyboardEventInit where toFFI = id
137 |
138 | export
139 | FromFFI KeyboardEventInit KeyboardEventInit where fromFFI = Just
140 |
141 | export data MouseEventInit : Type where [external]
142 |
143 | export
144 | ToFFI MouseEventInit MouseEventInit where toFFI = id
145 |
146 | export
147 | FromFFI MouseEventInit MouseEventInit where fromFFI = Just
148 |
149 | export data UIEventInit : Type where [external]
150 |
151 | export
152 | ToFFI UIEventInit UIEventInit where toFFI = id
153 |
154 | export
155 | FromFFI UIEventInit UIEventInit where fromFFI = Just
156 |
157 | export data WheelEventInit : Type where [external]
158 |
159 | export
160 | ToFFI WheelEventInit WheelEventInit where toFFI = id
161 |
162 | export
163 | FromFFI WheelEventInit WheelEventInit where fromFFI = Just
164 |