
  0 | module Web.Async.Confirm
  1 | 
  2 | import Derive.Prelude
  3 | import Text.HTML.DomID
  4 | import Web.Async
  5 | import Web.Async.Form
  6 | 
  7 | %default total
  8 | %language ElabReflection
  9 | 
 10 | public export
 11 | data ConfirmEv = Cancel | OK
 12 | 
 13 | %runElab derive "ConfirmEv" [Show,Eq,Ord]
 14 | 
 15 | confirm : ConfirmEv -> EditRes e -> Maybe (Maybe e)
 16 | confirm OK     (Valid v) = Just (Just v)
 17 | confirm Cancel _         = Just Nothing
 18 | confirm _      _         = Nothing
 19 | 
 20 | confirmStream :
 21 |      Sink (EditRes e)
 22 |   -> JSStream ConfirmEv
 23 |   -> JSStream (EditRes e)
 24 |   -> JSStream (Maybe e)
 25 | confirmStream ref cs es =
 26 |   resource (hold1 $ es |> observe sink) $ \esh =>
 27 |     zipWith confirm cs esh.stream |> P.catMaybes
 28 | 
 29 | ||| Wraps and editor in a parent node with buttons (or similar
 30 | ||| interactive elements) for cancellation and confirmation.
 31 | |||
 32 | ||| The resulting stream will pass on editing results, so that
 33 | ||| the buttons can be adjusted (for instance, disabled) accordingly.
 34 | |||
 35 | ||| The resulting stream fires only `Valid` events: `Nothing` in case
 36 | ||| of cancellation and `Just v` in case of confirmation.
 37 | |||
 38 | ||| See also `confirmed1` for a version that only ever fires one event
 39 | ||| at most.
 40 | export
 41 | confirmed :
 42 |      (wrap : HTMLNode -> Act (Sink (EditRes e), Widget ConfirmEv))
 43 |   -> Editor e
 44 |   -> Maybe e
 45 |   -> Act (Widget $ Maybe e)
 46 | confirmed wrap ed m = Prelude.do
 47 |   W inner es        <- ed.widget m
 48 |   (btn, W outer cs) <- wrap inner
 49 |   pure (W outer $ confirmStream btn cs es)
 50 | 
 51 | ||| Like `confirmed` but the resulting stream fires only at most one
 52 | ||| event.
 53 | export
 54 | confirmed1 :
 55 |      (wrap : HTMLNode -> Act (Sink (EditRes e), Widget ConfirmEv))
 56 |   -> Editor e
 57 |   -> Maybe e
 58 |   -> Act (Widget $ Maybe e)
 59 | confirmed1 wrap ed = map {events $= take 1} . confirmed wrap ed
 60 | 
 61 | export
 62 | keyConfirmed : Editor e -> Maybe e -> Act (Widget $ Maybe e)
 63 | keyConfirmed =
 64 |   confirmed $ \n => Prelude.do
 65 |     E es <- event {fs = [JSErr]} ConfirmEv
 66 |     let n2 := withAttributes [onEscDown Confirm.Cancel, onEnterDown OK] n
 67 |     pure (neutral, W n2 es)
 68 | 
 69 | export
 70 | cleanupDialog : DomID -> Act ()
 71 | cleanupDialog d =
 72 |   let ref := elemRef d
 73 |    in children ref [] >> dialogClose ref
 74 | 
 75 | export
 76 | confirmedModal :
 77 |      (wrap : HTMLNode -> Act (Sink (EditRes e), Widget ConfirmEv))
 78 |   -> DomID
 79 |   -> Editor e
 80 |   -> Maybe e
 81 |   -> Act (JSStream $ Maybe e)
 82 | confirmedModal wrap d ed m = Prelude.do
 83 |   let ref := elemRef d
 84 |   W n evs <- confirmed wrap ed m
 85 |   replace ref n
 86 |   showModal ref
 87 |   pure $ flip observe evs $ \case
 88 |     Nothing => cleanupDialog d
 89 |     _       => pure ()
 90 |