Idris2Doc : Web.Async.Util

Web.Async.Util

(source)
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__nextSibling : ChildNode -> PrimIO (Nullable ChildNode)
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
data Reader : Type
  Totality: total
  Visibility: export
  Hint: 
Resource (Async JS) Reader
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
removeTill : HasIO io => ChildNode -> ChildNode -> io ()
  Replaces all siblings after the first onde until the second
  is encountered.

  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
read : Elem JSErr es => Reader -> Async JS es (Maybe AnyBuffer)
  Totality: total
  Visibility: export