blob: 96d0cfac72a3ec9e7ebc84abaf6af9054ad0a90c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
import Wayland.Display
namespace Wayland.Protocols
abbrev RiverXkbBindingsV1.name : InterfaceName := "river_xkb_bindings_v1"
abbrev RiverXkbBindingV1.name : InterfaceName := "river_xkb_binding_v1"
abbrev RiverXkbBindingsSeatV1.name : InterfaceName := "river_xkb_bindings_seat_v1"
abbrev RiverXkbBindingsV1 : Type := Object RiverXkbBindingsV1.name
abbrev RiverXkbBindingV1 : Type := Object RiverXkbBindingV1.name
abbrev RiverXkbBindingsSeatV1 : Type := Object RiverXkbBindingsSeatV1.name
inductive RiverXkbBindingsV1.Error where
| objectAlreadyCreated
namespace RiverXkbBindingsV1.Error
instance : Marshallable RiverXkbBindingsV1.Error where
marshal
| .int, .objectAlreadyCreated => ArgumentMarshaller.marshalInt 0
| .uint, .objectAlreadyCreated => ArgumentMarshaller.marshalUInt 0
| _, _ => throw "Marshalling unexpected type, expected int or uint."
demarshal
| .int => do
match (← ArgumentDemarshaller.demarshalInt) with
| 0 => pure .objectAlreadyCreated
| _ => throw "Invalid enum value."
| .uint => do
match (← ArgumentDemarshaller.demarshalUInt) with
| 0 => pure .objectAlreadyCreated
| _ => throw "Invalid enum value."
| _ => throw "Demarshalling unexpected type, expected int or uint."
end RiverXkbBindingsV1.Error
end Wayland.Protocols
|
