JS.Attribute

Definitions

data Attribute : Bool -> (Type -> Type) -> Type -> Type

  A read-write attribute of a JS object.
  
  @alwaysReturns : Bool index if the attribute's getter can
                   always return a value that is neither
                   `null` nor `undefined`. This means, that the
                   attribute is non-nullable and either mandatory
                   or optional with a proper default value.
  
  @f             : Context of values represented by the attribute.
                   This is `Maybe` if the attribute is nullable,
                   `Optional` if it is an optional attribute on
                   a dictionary type, or `id` if it is mandatory
                   and non-nullable.
  
  @              : Type of values stored in the attribute

Totality: total
Visibility: public export
Constructors:

Attr : JSIO a -> (a -> JSIO ()) -> Attribute True id a

  A non-optional attribute.
  
  This is for data types, which are guaranteed to always return
  a value that is neither `null` nor `undefined`.

NullableAttr : JSIO (Maybe a) -> (Maybe a -> JSIO ()) -> Attribute False Maybe a

  A nullable, non-optional attribute.

OptionalAttr : JSIO (Optional a) -> (Optional a -> JSIO ()) -> a -> Attribute True Optional a

  An optional attribute with a predefined default value.

OptionalAttrNoDefault : JSIO (Optional a) -> (Optional a -> JSIO ()) -> Attribute False Optional a

  An optional attribute without default value.

get : obj -> (obj -> Attribute b f a) -> JSIO (f a)

  Returns the value of an attribute in its proper context.
  Typically used in infix notation.
  
  ```idris example
  textField `get` value
  ```

Totality: total
Visibility: export

over : (a -> b) -> Attribute x f a -> JSIO (f b)

  Maps a function over the value retrieved from an `Attribute`.

Totality: total
Visibility: export

to : (obj -> Attribute b f a) -> obj -> JSIO (f a)

  Flipped version of `get`. This is useful when
  combined with the bind operator:
  
  ```idris example
  body >>= to className
  ```

Totality: total
Visibility: export

set' : Attribute b f a -> f a -> JSIO ()

  Sets the value of an `Attribute`.

Totality: total
Visibility: export

getDef : obj -> (obj -> Attribute True f a) -> JSIO a

  Gets the value of an `Attribute`. Since this operates
  on an `Attribute True`, it is guaranteed to always yield
  a non-nullable value.

Totality: total
Visibility: export

overDef : (a -> b) -> Attribute True f a -> JSIO b

  Maps a function over the value retrieved from an `Attribute`.
  Since this operates
  on an `Attribute True`, it is guaranteed to always yield
  a non-nullable value.

Totality: total
Visibility: export

toDef : (obj -> Attribute True f a) -> obj -> JSIO a

  Flipped version of `getDef`.

Totality: total
Visibility: export

set : Attribute b f a -> a -> JSIO ()

  Sets the value of an `Attribute`.
  
  ```idris example
  disabled btn `set` True
  ```

Totality: total
Visibility: export

mod : Attribute b f a -> (a -> a) -> JSIO ()

  Modifies the stored value of an `Attribute`.
  
  Please note, that this will NOT change the attribute's
  values, if the attribute is unset or `null`.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 9

unset : Alternative f => obj -> (obj -> Attribute b f a) -> JSIO ()

  Unsets the value of an optional or nullable attribute.

Totality: total
Visibility: export

(.=) : Attribute b f a -> a -> JSIO ()

  Operator version of `set`.
  
  ```idris example
  disabled btn .= True
  ```

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1

(%=) : Attribute b f a -> (a -> a) -> JSIO ()

  Operator version of `mod`.
  
  As with `mod`, this will NOT change the attribute's
  values, if the attribute is unset or `null`.
  
  ```idris example
  toggleCheckBox : HTMLInputElement -> JSIO ()
  toggleCheckBox cbx = checked cbx %= not
  ```

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1

(=.) : (obj -> Attribute b f a) -> a -> obj -> JSIO ()

  Like `set`, but useful when the object, on which
  an attribute should operate, is supposed to
  be the last argument (for instance, when
  iterating over a foldable):
  
  ```idris example
  disableAll : List HTMLButtonElement -> JSIO ()
  disableAll buttons = for_ buttons $ disabled =. True
  ```

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1

(=%) : (obj -> Attribute b f a) -> (a -> a) -> obj -> JSIO ()

  Like `mod`, but useful when the object, on which
  an attribute should operate, is supposed to
  be the last argument (for instance, when
  iterating over a foldable):
  
  ```idris example
  toggleAll : List HTMLInputElement -> JSIO ()
  toggleAll cbxs = for_ cbxs $ checked =% not
  ```

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1

(!>) : Callback a fun => Attribute b f a -> fun -> JSIO ()

  Sets a callback function at an attribute.
  
  ```idris
  onclick btn !> consoleLog . jsShow
  ```

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 0

(?>) : Callback a (x -> y) => Attribute b f a -> y -> JSIO ()

  Sets a callback action at an attribute. This is like `(!>)`
  but ignores its input.
  
  ```idris
  onclick btn ?> consoleLog "Boom!"
  ```

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 0

fromPrim : ToFFI a b => FromFFI a b => String -> (obj -> PrimIO b) -> (obj -> b -> PrimIO ()) -> obj -> Attribute True id a

Totality: total
Visibility: export

fromNullablePrim : ToFFI a b => FromFFI a b => String -> (obj -> PrimIO (Nullable b)) -> (obj -> Nullable b -> PrimIO ()) -> obj -> Attribute False Maybe a

Totality: total
Visibility: export

fromUndefOrPrim : ToFFI a b => FromFFI a b => String -> (obj -> PrimIO (UndefOr b)) -> (obj -> UndefOr b -> PrimIO ()) -> a -> obj -> Attribute True Optional a

Totality: total
Visibility: export

fromUndefOrPrimNoDefault : ToFFI a b => FromFFI a b => String -> (obj -> PrimIO (UndefOr b)) -> (obj -> UndefOr b -> PrimIO ()) -> obj -> Attribute False Optional a

Totality: total
Visibility: export