Idris2Doc : Web.Dom

Web.Dom

(source)

Reexports

import public Web.Internal.Types
import public Web.Raw.Dom as Dom

Definitions

window : JSIO Window
Totality: total
Visibility: export
document : JSIO Document
Totality: total
Visibility: export
body : JSIO HTMLElement
Totality: total
Visibility: export
0 Anchor : Type
Totality: total
Visibility: public export
0 Area : Type
Totality: total
Visibility: public export
0 Audio : Type
Totality: total
Visibility: public export
0 BR : Type
Totality: total
Visibility: public export
0 Base : Type
Totality: total
Visibility: public export
0 Body : Type
Totality: total
Visibility: public export
0 Button : Type
Totality: total
Visibility: public export
0 Canvas : Type
Totality: total
Visibility: public export
0 DList : Type
Totality: total
Visibility: public export
0 Data : Type
Totality: total
Visibility: public export
0 DataList : Type
Totality: total
Visibility: public export
0 Details : Type
Totality: total
Visibility: public export
0 Dialog : Type
Totality: total
Visibility: public export
0 Div : Type
Totality: total
Visibility: public export
0 Embed : Type
Totality: total
Visibility: public export
0 FieldSet : Type
Totality: total
Visibility: public export
0 Form : Type
Totality: total
Visibility: public export
0 HR : Type
Totality: total
Visibility: public export
0 Heading : Type
Totality: total
Visibility: public export
0 Html : Type
Totality: total
Visibility: public export
0 IFrame : Type
Totality: total
Visibility: public export
0 Image : Type
Totality: total
Visibility: public export
0 Input : Type
Totality: total
Visibility: public export
0 LI : Type
Totality: total
Visibility: public export
0 Label : Type
Totality: total
Visibility: public export
0 Legend : Type
Totality: total
Visibility: public export
Totality: total
Visibility: public export
0 Map : Type
Totality: total
Visibility: public export
0 Menu : Type
Totality: total
Visibility: public export
0 Meta : Type
Totality: total
Visibility: public export
0 Meter : Type
Totality: total
Visibility: public export
0 Mod : Type
Totality: total
Visibility: public export
0 OList : Type
Totality: total
Visibility: public export
0 Object : Type
Totality: total
Visibility: public export
0 OptGroup : Type
Totality: total
Visibility: public export
0 Option : Type
Totality: total
Visibility: public export
0 Output : Type
Totality: total
Visibility: public export
0 Paragraph : Type
Totality: total
Visibility: public export
0 Param : Type
Totality: total
Visibility: public export
0 Picture : Type
Totality: total
Visibility: public export
0 Pre : Type
Totality: total
Visibility: public export
0 Progress : Type
Totality: total
Visibility: public export
0 Quote : Type
Totality: total
Visibility: public export
0 Script : Type
Totality: total
Visibility: public export
0 Select : Type
Totality: total
Visibility: public export
0 Slot : Type
Totality: total
Visibility: public export
0 Source : Type
Totality: total
Visibility: public export
0 Span : Type
Totality: total
Visibility: public export
0 Style : Type
Totality: total
Visibility: public export
0 TableCaption : Type
Totality: total
Visibility: public export
0 TableCell : Type
Totality: total
Visibility: public export
0 TableCol : Type
Totality: total
Visibility: public export
0 Table : Type
Totality: total
Visibility: public export
0 TableRow : Type
Totality: total
Visibility: public export
0 TableSection : Type
Totality: total
Visibility: public export
0 Template : Type
Totality: total
Visibility: public export
0 TextArea : Type
Totality: total
Visibility: public export
0 Time : Type
Totality: total
Visibility: public export
0 Title : Type
Totality: total
Visibility: public export
0 Track : Type
Totality: total
Visibility: public export
0 UList : Type
Totality: total
Visibility: public export
0 Video : Type
Totality: total
Visibility: public export
data ElementType : String -> Type -> Type
  HTML Element Tags linking tag names with HTML element types

This is mainly to be used with `Web.Dom.createElement` and `newElement`.
Some deprecated tags have been left out, some others might
still be missing.

Totality: total
Visibility: public export
Constructors:
A : ElementType "a" HTMLAnchorElement
Address : ElementType "address" HTMLElement
Area : ElementType "area" HTMLAreaElement
Article : ElementType "article" HTMLElement
Audio : ElementType "audio" HTMLAudioElement
Base : ElementType "base" HTMLBaseElement
Blockquote : ElementType (fromString "blockquote") HTMLQuoteElement
Body : ElementType "body" HTMLBodyElement
Br : ElementType "br" HTMLBRElement
Button : ElementType "button" HTMLButtonElement
Canvas : ElementType "canvas" HTMLCanvasElement
Caption : ElementType "caption" HTMLTableCaptionElement
Col : ElementType "col" HTMLTableColElement
Colgroup : ElementType "colgroup" HTMLTableColElement
Data : ElementType "data" HTMLDataElement
Datalist : ElementType "datalist" HTMLDataListElement
Del : ElementType "del" HTMLModElement
Details : ElementType "details" HTMLDetailsElement
Dialog : ElementType "dialog" HTMLDialogElement
Div : ElementType "div" HTMLDivElement
Dl : ElementType "dl" HTMLDListElement
Embed : ElementType "embed" HTMLEmbedElement
FieldSet : ElementType "fieldset" HTMLFieldSetElement
Footer : ElementType "footer" HTMLElement
Form : ElementType "form" HTMLFormElement
H1 : ElementType "h1" HTMLHeadingElement
H2 : ElementType "h2" HTMLHeadingElement
H3 : ElementType "h3" HTMLHeadingElement
H4 : ElementType "h4" HTMLHeadingElement
H5 : ElementType "h5" HTMLHeadingElement
H6 : ElementType "h6" HTMLHeadingElement
HR : ElementType "hr" HTMLHRElement
Header : ElementType "header" HTMLElement
Html : ElementType "html" HTMLHtmlElement
IFrame : ElementType "iframe" HTMLIFrameElement
Img : ElementType "img" HTMLImageElement
Input : ElementType "input" HTMLInputElement
Ins : ElementType "ins" HTMLModElement
Label : ElementType "label" HTMLLabelElement
Legend : ElementType "legend" HTMLLegendElement
Li : ElementType "li" HTMLLIElement
Map : ElementType "map" HTMLMapElement
Menu : ElementType "menu" HTMLMenuElement
Meta : ElementType "meta" HTMLMetaElement
Meter : ElementType "meter" HTMLMeterElement
Object : ElementType "object" HTMLObjectElement
Ol : ElementType "ol" HTMLOListElement
OptGroup : ElementType "optgroup" HTMLOptGroupElement
Option : ElementType "option" HTMLOptionElement
Output : ElementType "output" HTMLOutputElement
P : ElementType "p" HTMLParagraphElement
Param : ElementType "param" HTMLParamElement
Picture : ElementType "picture" HTMLPictureElement
Pre : ElementType "pre" HTMLPreElement
Progress : ElementType "progress" HTMLProgressElement
Q : ElementType "q" HTMLQuoteElement
Script : ElementType "script" HTMLScriptElement
Section : ElementType "section" HTMLElement
Select : ElementType "select" HTMLSelectElement
Slot : ElementType "slot" HTMLSlotElement
Source : ElementType "source" HTMLSourceElement
Span : ElementType "span" HTMLSpanElement
Style : ElementType "style" HTMLStyleElement
Table : ElementType "table" HTMLTableElement
Tbody : ElementType "tbody" HTMLTableSectionElement
Td : ElementType "td" HTMLTableCellElement
Template : ElementType "template" HTMLTemplateElement
TextArea : ElementType "textarea" HTMLTextAreaElement
Tfoot : ElementType "tfoot" HTMLTableSectionElement
Th : ElementType "th" HTMLTableCellElement
Thead : ElementType "thead" HTMLTableSectionElement
Time : ElementType "time" HTMLTimeElement
Title : ElementType "title" HTMLTitleElement
Tr : ElementType "tr" HTMLTableRowElement
Track : ElementType "track" HTMLTrackElement
Ul : ElementType "ul" HTMLUListElement
Video : ElementType "video" HTMLVideoElement
elementTag : (0 _ : ElementType tag t) -> String
  Extracts the `tag` String from a known `ElementType`.

Totality: total
Visibility: public export
createElement : SafeCast t => (0 _ : ElementType tag t) -> JSIO t
  Creates a new element using the given `ElementType`'s `tag`
and casting the result to the corresponding HTML element type.
See also `newElement`.

Totality: total
Visibility: export
newElement : SafeCast t => (0 _ : ElementType tag t) -> List (t -> JSIO ()) -> JSIO t
  Like `createElement` but applies the given set of
modifiers. This is especially useful for setting an element's
attributes.

Totality: total
Visibility: export
getElementById : String -> JSIO (Maybe Element)
Totality: total
Visibility: export
castElementById_ : SafeCast a => String -> JSIO (Maybe a)
Totality: total
Visibility: export
castElementById : (0 a : Type) -> SafeCast a => String -> JSIO (Maybe a)
Totality: total
Visibility: export
htmlElementById : SafeCast t => (0 _ : ElementType tag t) -> String -> JSIO (Maybe t)
Totality: total
Visibility: export
getElementsByClass : String -> JSIO HTMLCollection
Totality: total
Visibility: export
firstElementByClass : String -> JSIO (Maybe Element)
Totality: total
Visibility: export
castFirstElementByClass_ : SafeCast a => String -> JSIO (Maybe a)
Totality: total
Visibility: export
castFirstElementByClass : (0 a : Type) -> SafeCast a => String -> JSIO (Maybe a)
Totality: total
Visibility: export
firstHtmlElementByClass : (0 _ : ElementType tag a) -> SafeCast a => String -> JSIO (Maybe a)
Totality: total
Visibility: export
getElementByClass : SafeCast t => String -> JSIO t
  Tries to retrieve an element of the given type by looking
up its class in the DOM. Unlike `firstElementByClass`, this will throw
an exception in the `JSIO` monad if the element is not found
or can't be safely cast to the desired type.

Totality: total
Visibility: export