blob: 7c01f9056872c3331d70cc3e08fcf72ead116fa8 (
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 RiverLayerShellV1.name : InterfaceName := "river_layer_shell_v1"
abbrev RiverLayerShellOutputV1.name : InterfaceName := "river_layer_shell_output_v1"
abbrev RiverLayerShellSeatV1.name : InterfaceName := "river_layer_shell_seat_v1"
abbrev RiverLayerShellV1 : Type := Object RiverLayerShellV1.name
abbrev RiverLayerShellOutputV1 : Type := Object RiverLayerShellOutputV1.name
abbrev RiverLayerShellSeatV1 : Type := Object RiverLayerShellSeatV1.name
inductive RiverLayerShellV1.Error where
| objectAlreadyCreated
namespace RiverLayerShellV1.Error
instance : Marshallable RiverLayerShellV1.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 RiverLayerShellV1.Error
end Wayland.Protocols
|
