blob: 6cbdaab0a05b04e2cc37b83401dd2d61ec1d0a8b (
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
import Wayland.Display
import Wayland.Protocols.RiverLayerShellV1.Resolved
import Wayland.Protocols.RiverWindowManagementV1.Header
namespace Wayland.Protocols
variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
def RiverLayerShellV1.destroy
(ω : RiverLayerShellV1)
: DisplayM σ Unit :=
ω.send true do
return 0
def RiverLayerShellV1.getOutput
(ω : RiverLayerShellV1)
(output : RiverOutputV1)
: DisplayM σ RiverLayerShellOutputV1 :=
ω.sendConstructor false do
ArgumentMarshaller.marshalAnyObject .none
Marshallable.marshal .object output
return 1
def RiverLayerShellV1.getSeat
(ω : RiverLayerShellV1)
(seat : RiverSeatV1)
: DisplayM σ RiverLayerShellSeatV1 :=
ω.sendConstructor false do
ArgumentMarshaller.marshalAnyObject .none
Marshallable.marshal .object seat
return 2
def RiverLayerShellOutputV1.destroy
(ω : RiverLayerShellOutputV1)
: DisplayM σ Unit :=
ω.send true do
return 0
def RiverLayerShellOutputV1.setDefault
(ω : RiverLayerShellOutputV1)
: DisplayM σ Unit :=
ω.send false do
return 1
def RiverLayerShellSeatV1.destroy
(ω : RiverLayerShellSeatV1)
: DisplayM σ Unit :=
ω.send true do
return 0
end Wayland.Protocols
|
