
  0 | module Text.HTML.Confirm
  1 | 
  2 | import Text.HTML
  3 | import Text.HTML.Class
  4 | import Text.HTML.DomID
  5 | 
  6 | %default total
  7 | 
  8 | public export
  9 | data ConfirmEv : Type -> Type where
 10 |   Cancel : ConfirmEv e
 11 |   Begin  : ConfirmEv e
 12 |   Edited : (event : e) -> ConfirmEv e
 13 |   OK     : ConfirmEv e
 14 | 
 15 | ||| Environment for beginning an editing process.
 16 | public export
 17 | record ConfirmConfig (i : Type) where
 18 |   [noHints]
 19 |   constructor CC
 20 |   title      : String
 21 |   listCls    : Class
 22 |   titleCls   : Class
 23 |   rowCls     : Class
 24 |   okID       : i -> i
 25 |   okNode     : {0 e : _} -> i -> e -> Node e
 26 |   cancelNode : {0 e : _} -> e -> Node e
 27 | 
 28 | parameters {0 i, e : Type}
 29 |            {auto cst : Cast i DomID}
 30 |            (ce  : ConfirmConfig i)
 31 | 
 32 |   export
 33 |   dialog : i -> Node e -> Node (ConfirmEv e)
 34 |   dialog u n =
 35 |     list ce.listCls []
 36 |       [ div [cls Title ce.titleCls] [Text ce.title]
 37 |       , Edited <$> n
 38 |       , row ce.rowCls [] [ ce.okNode (ce.okID u) OK, ce.cancelNode Cancel]
 39 |       ]
 40 |