Web.Async.Util

Reexports

import public FS
import public FS.Concurrent.Signal
import public IO.Async.JS
import public JS
import public Text.HTML

Definitions

prim__append : ParentNode -> Node -> PrimIO ()

prim__appendTxt : ParentNode -> String -> PrimIO ()

prim__remove : ChildNode -> PrimIO ()

prim__createElement : String -> PrimIO Element

prim__setAttribute : Element -> String -> String -> PrimIO ()

prim__removeAttribute : Element -> String -> PrimIO ()

prim__innerHTML : InnerHTML -> PrimIO String

prim__setInnerHTML : InnerHTML -> String -> PrimIO ()

prim__content : HTMLTemplateElement -> PrimIO DocumentFragment

prim__createDocumentFragment : PrimIO DocumentFragment

prim__setChecked : HTMLInputElement -> Boolean -> PrimIO ()

prim__checked : HTMLInputElement -> PrimIO Bool

window : HasIO io => io Window

  Return the current window.

Totality: total
Visibility: export

document : HasIO io => io Document

  Return the current document.

Totality: total
Visibility: export

getBody : HasIO io => io (Maybe HTMLElement)

  Return the body element of the current document.
  
  Return `Nothing` in case the current document has no body defined.

Totality: total
Visibility: export

click : HasIO io => HTMLElement -> io ()

  Simulates a mouse click on an element.

Totality: total
Visibility: export

replaceChildren : HasIO io => ParentNode -> Node -> io ()

  Replace all children of the given node with a new node.

Totality: total
Visibility: export

append : HasIO io => ParentNode -> Node -> io ()

  Append the given node to a DOM element's children

Totality: total
Visibility: export

prepend : HasIO io => ParentNode -> Node -> io ()

  Prepend the given node to a DOM element's children

Totality: total
Visibility: export

after : HasIO io => ChildNode -> Node -> io ()

  Insert the given node after a DOM element

Totality: total
Visibility: export

before : HasIO io => ChildNode -> Node -> io ()

  Insert the given node before a DOM element

Totality: total
Visibility: export

replace : HasIO io => ChildNode -> Node -> io ()

  Replace a DOM element with the given node.

Totality: total
Visibility: export

remove : HasIO io => ChildNode -> io ()

  Replace a DOM element with the given document fragment.

Totality: total
Visibility: export

createElement : HasIO io => String -> io Element

  Creates a DOM element of the given type.

Totality: total
Visibility: export

setAttribute : HasIO io => Element -> String -> String -> io ()

  Sets an attribute of a DOM element.

Totality: total
Visibility: export

removeAttribute : HasIO io => Element -> String -> io ()

  Unsets an attribute of a DOM element.

Totality: total
Visibility: export

innerHTML : HasIO io => InnerHTML -> io String

  Returns the inner HTML structure of a node as a String

Totality: total
Visibility: export

setInnerHTML : HasIO io => InnerHTML -> String -> io ()

  Sets the inner HTML structure of a node.

Totality: total
Visibility: export

focus : HasIO io => HTMLElement -> io ()

  Focus the given HTML element

Totality: total
Visibility: export

blur : HasIO io => HTMLElement -> io ()

  Blur (lose focus of) the given HTML element

Totality: total
Visibility: export

currentTime : HasIO io => io Integer

  Get the current time in milliseconds since 1970/01/01.

Totality: total
Visibility: export

timed : HasIO io => io t -> io (t, Integer)

  Determine the time taken to run an `IO` action.

Totality: total
Visibility: export

timed' : HasIO io => io () -> io Integer

Totality: total
Visibility: export

toClipboard : HasIO io => String -> io ()

  Writes as string to the clipboard.

Totality: total
Visibility: export

itemToClipboard : Elem JSErr es => ClipboardItem -> Async JS es ()

  Writes a `ClipboardItem` to the clipboard.

Totality: total
Visibility: export

clipboardItem : HasIO io => String -> String -> io ClipboardItem

  Wraps some text data plus its mimetype in a `ClipboardItem`

Totality: total
Visibility: export

dataToClipboard : Elem JSErr es => String -> String -> Async JS es ()

  Writes some text data plus its mimetype to the clipboard.

Totality: total
Visibility: export

readFromClipboard1 : HasIO io => (String -> IO1 ()) -> io ()

Totality: total
Visibility: export

readFromClipboard : Async e es String

Totality: total
Visibility: export

dialogShow : HasIO io => HTMLDialogElement -> io ()

  Show the given dialog element

Totality: total
Visibility: export

dialogClose : HasIO io => HTMLDialogElement -> io ()

  Close the given dialog element

Totality: total
Visibility: export

showModal : HasIO io => HTMLDialogElement -> io ()

  Show the given dialog element in "modal" mode

Totality: total
Visibility: export

interface ToBlob : Type -> Type

Parameters: a
Methods:

toBlob : a -> AnyPtr

Implementations:

ToBlob (IArray k String)
ToBlob (Array String)
ToBlob (List String)
ToBlob String

toBlob : ToBlob a => a -> AnyPtr

Totality: total
Visibility: public export

blob : HasIO io => ToBlob a => a -> String -> io Blob

Totality: total
Visibility: export

record ObjectURL : Type

  A URL (as a wrapped string) pointing to an object in memory.
  
  This should be treated as a resource and properly released via `cleanup`.

Totality: total
Visibility: export
Constructor:

OU : String -> ObjectURL

Projection:

.url : ObjectURL -> String

Hints:

Cast ObjectURL String
Resource (Async JS) ObjectURL

blobURL : HasIO io => Blob -> io ObjectURL

  Provides a URL pointing to the given `Blob` object.
  
  Use `cast` to convert the `ObjectURL` to a `String` and make sure to
  release it

Totality: total
Visibility: export

blobBytes : Has JSErr es => Blob -> Async JS es AnyBuffer

  Extracts the bytes from a `Blob`.

Totality: total
Visibility: export

0 ElemType : Ref t -> Type

  DOM type associacte with an ElemRef

Totality: total
Visibility: public export

0 JS : List Type -> Type -> Type

Totality: total
Visibility: public export

js : Has JSErr es => JSIO t -> JS es t

Totality: total
Visibility: export

jsCast : Has JSErr es => SafeCast t => String -> s -> JS es t

Totality: total
Visibility: export

unmaybe : Has JSErr es => Lazy String -> Maybe t -> JS es t

Totality: total
Visibility: export

body : Has JSErr es => JS es HTMLElement

Totality: total
Visibility: export

getElementById : Has JSErr es => SafeCast t => Maybe String -> String -> JS es t

  Tries to retrieve an element of the given type by looking
  up its ID in the DOM.
  
  This will throw a `JSErr` in case the element cannot be found
  or cast to the desired result type.

Totality: total
Visibility: export

getHTMLElementById : Has JSErr es => String -> String -> JS es HTMLElement

  Tries to retrieve a HTMLElement by looking
  
  This will throw a `JSErr` in case the element cannot be found
  or cast to the desired result type.

Totality: total
Visibility: export

getElementByRef : Has JSErr es => (r : Ref t) -> JS es (ElemType r)

  Tries to retrieve an element of the given type by looking
  up its ID in the DOM.
  
  This will throw a `JSErr` in case the element cannot be found
  or cast to the desired result type.

Totality: total
Visibility: export

castElementByRef : Has JSErr es => SafeCast t => Ref x -> JS es t

  Tries to retrieve an element of the given type by looking
  up its ID in the DOM.
  
  This will throw a `JSErr` in case the element cannot be found
  or cast to the desired result type.

Totality: total
Visibility: export

validityMessage : Has JSErr es => Ref t -> {auto 0 _ : ValidityTag t} -> String -> JS es ()

  Sets a custom validity message at the given reference.
  
  Pass the empty string to mark the element as valid.
  
  This will throw a `JSErr` in case the element cannot be found
  or cast to the desired result type.

Totality: total
Visibility: export

validate : Has JSErr es => Ref t -> {auto 0 _ : ValidityTag t} -> Either String b -> JS es ()

  Sets or unsets a custom validity message at the given node.

Totality: total
Visibility: export

setValue : Has JSErr es => Ref t -> {auto 0 _ : ValueTag t} -> String -> JS es ()

  Sets the value of the element identified by the given ID.
  
  This will throw a `JSErr` in case the element cannot be found
  or cast to the desired result type.

Totality: total
Visibility: export

0 Act : Type -> Type

Totality: total
Visibility: public export

0 JSPull : Type -> Type -> Type

Totality: total
Visibility: public export

0 JSStream : Type -> Type

Totality: total
Visibility: public export

pullErr : AsyncStream f es Void -> Async f es ()

Visibility: export

runJS : JS [JSErr] () -> IO ()

Visibility: export

runProg : JSStream Void -> IO ()

Visibility: export

mvcActEvs : JSStream e -> s -> (e -> s -> Act s) -> JSStream Void

Totality: total
Visibility: export

mvcAct : e -> s -> (Sink e => e -> s -> Act s) -> JSStream Void

Totality: total
Visibility: export

mvc : e -> s -> (e -> s -> s) -> (Sink e => e -> s -> Act ()) -> JSStream Void

Totality: total
Visibility: export

getClientRect : LIO f => Element -> f Rect

Totality: total
Visibility: export