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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
import Wayland.Display
import Wayland.Protocols.RiverLayerShellV1.Header
namespace Wayland.Protocols
inductive RiverLayerShellV1.Event where
inductive RiverLayerShellOutputV1.Event where
| nonExclusiveArea
(x : Int32)
(y : Int32)
(width : Int32)
(height : Int32)
inductive RiverLayerShellSeatV1.Event where
| focusExclusive
| focusNonExclusive
| focusNone
instance instInterfaceRiverLayerShellV1 : Interface RiverLayerShellV1.name where
event := RiverLayerShellV1.Event
version := 1
requests := #[
{
name := "destroy"
args := #[]
since := 1
isDestructor := true
},
{
name := "get_output"
args := #[.newID (.some "river_layer_shell_output_v1"), .object .notNull (.some "river_output_v1")]
since := 1
isDestructor := false
},
{
name := "get_seat"
args := #[.newID (.some "river_layer_shell_seat_v1"), .object .notNull (.some "river_seat_v1")]
since := 1
isDestructor := false
},
]
events := #[
]
demarshalEvent
| _ => throw s!"Received invalid opcode"
instance instInterfaceRiverLayerShellOutputV1 : Interface RiverLayerShellOutputV1.name where
event := RiverLayerShellOutputV1.Event
version := 1
requests := #[
{
name := "destroy"
args := #[]
since := 1
isDestructor := true
},
{
name := "set_default"
args := #[]
since := 1
isDestructor := false
},
]
events := #[
{
name := "non_exclusive_area"
args := #[.int, .int, .int, .int]
since := 1
isDestructor := false
},
]
demarshalEvent
| 0 => do
return .nonExclusiveArea
(← Marshallable.demarshal .int)
(← Marshallable.demarshal .int)
(← Marshallable.demarshal .int)
(← Marshallable.demarshal .int)
| _ => throw s!"Received invalid opcode"
instance instInterfaceRiverLayerShellSeatV1 : Interface RiverLayerShellSeatV1.name where
event := RiverLayerShellSeatV1.Event
version := 1
requests := #[
{
name := "destroy"
args := #[]
since := 1
isDestructor := true
},
]
events := #[
{
name := "focus_exclusive"
args := #[]
since := 1
isDestructor := false
},
{
name := "focus_non_exclusive"
args := #[]
since := 1
isDestructor := false
},
{
name := "focus_none"
args := #[]
since := 1
isDestructor := false
},
]
demarshalEvent
| 0 => do
return .focusExclusive
| 1 => do
return .focusNonExclusive
| 2 => do
return .focusNone
| _ => throw s!"Received invalid opcode"
end Wayland.Protocols
|