0 | module Text.HTML.File
 1 |
 2 | import Text.HTML
 3 | import Text.HTML.Class
 4 | import Text.HTML.DomID
 5 | import Text.HTML.Validation
 6 | import public Data.FilePath
 7 | import public Web.Internal.FileTypes
 8 |
 9 | %default total
10 |
11 | public export
12 | data FileEv : Type where
13 |   NameChanged : String -> FileEv
14 |   FileChanged : File -> String -> FileEv
15 |
16 | ||| Environment for editing files plus their paths
17 | public export
18 | record FileEnv (i : Type) where
19 |   [noHints]
20 |   constructor FE
21 |   fileID    : i -> i
22 |   readBody  : String -> Either String Body
23 |   browse    : String
24 |   fileCls   : Class
25 |   inputCls  : Class
26 |   labelCls  : Class
27 |
28 | fromInfo : InputInfo -> Maybe FileEv
29 | fromInfo (MkInputInfo v [f] checked) = Just (FileChanged f v)
30 | fromInfo _                           = Nothing
31 |
32 | parameters {0      i : Type}
33 |            {auto cst : Cast i DomID}
34 |            {auto ve  : ValEnv i}
35 |            {auto fe  : FileEnv i}
36 |
37 |   export
38 |   file : (fe : FileEnv i) => i -> Maybe Body -> Node FileEv
39 |   file uid (Just b) = NameChanged <$> vinp fe.inputCls Text uid "\{b}"
40 |   file uid Nothing  =
41 |     cell fe.fileCls []
42 |       [ NameChanged <$> vinp fe.inputCls Text uid ""
43 |       , label [forID (fe.fileID uid), cls Btn fe.labelCls] [Text fe.browse]
44 |       , input
45 |           [ ref $ fe.fileID uid
46 |           , cls Widget fe.fileCls
47 |           , type File
48 |           , Event (Input fromInfo)
49 |           ] []
50 |       ]
51 |