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