0 | module Web.Internal.FileTypes
  1 |
  2 | import JS
  3 |
  4 | %default total
  5 |
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --          Enums
  9 | --------------------------------------------------------------------------------
 10 |
 11 | namespace EndingType
 12 |
 13 |   public export
 14 |   data EndingType = Transparent | Native
 15 |
 16 |   public export
 17 |   Show EndingType where
 18 |     show Transparent = "transparent"
 19 |     show Native = "native"
 20 |
 21 |   public export
 22 |   Eq EndingType where
 23 |     (==) = (==) `on` show
 24 |
 25 |   public export
 26 |   Ord EndingType where
 27 |     compare = compare `on` show
 28 |
 29 |   public export
 30 |   read : String -> Maybe EndingType
 31 |   read "transparent" = Just Transparent
 32 |   read "native" = Just Native
 33 |   read _ = Nothing
 34 |
 35 |   export
 36 |   ToFFI EndingType String where
 37 |     toFFI = show
 38 |
 39 |   export
 40 |   FromFFI EndingType String where
 41 |     fromFFI = read
 42 |
 43 |
 44 |
 45 | --------------------------------------------------------------------------------
 46 | --          Interfaces
 47 | --------------------------------------------------------------------------------
 48 |
 49 | export data Blob : Type where [external]
 50 |
 51 | export
 52 | ToFFI Blob Blob where toFFI = id
 53 |
 54 | export
 55 | FromFFI Blob Blob where fromFFI = Just
 56 |
 57 | export
 58 | SafeCast Blob where
 59 |   safeCast = unsafeCastOnPrototypeName "Blob"
 60 |
 61 | export data File : Type where [external]
 62 |
 63 | export
 64 | ToFFI File File where toFFI = id
 65 |
 66 | export
 67 | FromFFI File File where fromFFI = Just
 68 |
 69 | export
 70 | SafeCast File where
 71 |   safeCast = unsafeCastOnPrototypeName "File"
 72 |
 73 | export data FileList : Type where [external]
 74 |
 75 | export
 76 | ToFFI FileList FileList where toFFI = id
 77 |
 78 | export
 79 | FromFFI FileList FileList where fromFFI = Just
 80 |
 81 | export
 82 | SafeCast FileList where
 83 |   safeCast = unsafeCastOnPrototypeName "FileList"
 84 |
 85 | export data FileReader : Type where [external]
 86 |
 87 | export
 88 | ToFFI FileReader FileReader where toFFI = id
 89 |
 90 | export
 91 | FromFFI FileReader FileReader where fromFFI = Just
 92 |
 93 | export
 94 | SafeCast FileReader where
 95 |   safeCast = unsafeCastOnPrototypeName "FileReader"
 96 |
 97 | export data FileReaderSync : Type where [external]
 98 |
 99 | export
100 | ToFFI FileReaderSync FileReaderSync where toFFI = id
101 |
102 | export
103 | FromFFI FileReaderSync FileReaderSync where fromFFI = Just
104 |
105 | export
106 | SafeCast FileReaderSync where
107 |   safeCast = unsafeCastOnPrototypeName "FileReaderSync"
108 |
109 |
110 | --------------------------------------------------------------------------------
111 | --          Dictionaries
112 | --------------------------------------------------------------------------------
113 |
114 | export data BlobPropertyBag : Type where [external]
115 |
116 | export
117 | ToFFI BlobPropertyBag BlobPropertyBag where toFFI = id
118 |
119 | export
120 | FromFFI BlobPropertyBag BlobPropertyBag where fromFFI = Just
121 |
122 | export data FilePropertyBag : Type where [external]
123 |
124 | export
125 | ToFFI FilePropertyBag FilePropertyBag where toFFI = id
126 |
127 | export
128 | FromFFI FilePropertyBag FilePropertyBag where fromFFI = Just
129 |