LeanReactSource on GitHub ↗

Example 04 / Try it

Let people finish typing.

Clear the title and try to save. Then type a new title and save again.

Live componentLEAN + REACT

This is a local demo. Nothing is sent to a server.

FormDemo.lean
def FormDemo : Component Unit := component fun _ => do
  let form ← useForm Tickets.titleParser "Fix the login page" "draft-title"
  let notice ← useState "" "save-notice"
  let save : Action Unit := do
    let result ← form.submit fun title => notice.set ("Saved: " ++ title.value)
    match result with
    | .ok _ => pure ()
    | .error errors => notice.set (Tickets.titleValidationMessage errors)
  pure <| DOM.div { className := some "form-demo" } #[
    DOM.label { htmlFor := "draft-title" } #[text "Ticket title"],
    DOM.input {
      id := some "draft-title", value := some form.binding.value,
      onChange := some (fun event => do form.binding.set event.value; notice.set "")
    },
    DOM.p { className := some "field-hint" } #[text "Use between 1 and 200 characters."],
    DOM.button { className := some "primary", onPress := some save } #[text "Save title"],
    DOM.p { role := some "status" } #[text notice.value]
  ]

The form keeps invalid text while you edit. The save callback runs only after the title passes validation.