blob: d20182e3bd64944b51e8098b04c6dd2aa266ee53 (
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
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
|
import Wayland.Display
import Wayland.Protocols.RiverInputManagementV1.Resolved
import Wayland.Protocols.Wayland.Header
namespace Wayland.Protocols
variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
def RiverInputManagerV1.stop
(ω : RiverInputManagerV1)
: DisplayM σ Unit :=
ω.send false do
return 0
def RiverInputManagerV1.destroy
(ω : RiverInputManagerV1)
: DisplayM σ Unit :=
ω.send true do
return 1
def RiverInputManagerV1.createSeat
(ω : RiverInputManagerV1)
(name : String)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .string name
return 2
def RiverInputManagerV1.destroySeat
(ω : RiverInputManagerV1)
(name : String)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .string name
return 3
def RiverInputDeviceV1.destroy
(ω : RiverInputDeviceV1)
: DisplayM σ Unit :=
ω.send true do
return 0
def RiverInputDeviceV1.assignToSeat
(ω : RiverInputDeviceV1)
(name : String)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .string name
return 1
def RiverInputDeviceV1.setRepeatInfo
(ω : RiverInputDeviceV1)
(rate : Int32)
(delay : Int32)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .int rate
Marshallable.marshal .int delay
return 2
def RiverInputDeviceV1.setScrollFactor
(ω : RiverInputDeviceV1)
(factor : Float32)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .fixed factor
return 3
def RiverInputDeviceV1.mapToOutput
(ω : RiverInputDeviceV1)
(output : Option WlOutput)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .object output
return 4
def RiverInputDeviceV1.mapToRectangle
(ω : RiverInputDeviceV1)
(x : Int32)
(y : Int32)
(width : Int32)
(height : Int32)
: DisplayM σ Unit :=
ω.send false do
Marshallable.marshal .int x
Marshallable.marshal .int y
Marshallable.marshal .int width
Marshallable.marshal .int height
return 5
end Wayland.Protocols
|
