blob: 430472bc73dfa7d5ff2b9e18b127c520c8f8fd7e (
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
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
variable {M : Type}
namespace Wayland.Native
structure Message where
name : String
signature : String
types : Array (Option String)
structure Interface where
name : String
version : UInt32
requests : Array Message
events : Array Message
private opaque DisplayP : NonemptyType
private opaque EventLoopP (M : Type) : NonemptyType
private opaque EventSourceP : NonemptyType
private opaque TypeMapP : NonemptyType
private opaque ArgumentBufferP : NonemptyType
private opaque ProxyP : NonemptyType
def Display : Type := DisplayP.type
def EventLoop (M : Type) : Type := (EventLoopP M).type
def EventSource : Type := EventSourceP.type
def TypeMap : Type := TypeMapP.type
def ArgumentBuffer : Type := ArgumentBufferP.type
def Proxy : Type := ProxyP.type
instance : Nonempty Display := DisplayP.property
instance : Nonempty (EventLoop M) := (EventLoopP M).property
instance : Nonempty EventSource := EventSourceP.property
instance : Nonempty TypeMap := TypeMapP.property
instance : Nonempty ArgumentBuffer := ArgumentBufferP.property
instance : Nonempty Proxy := ProxyP.property
@[extern "waylean_SIGINT"]
opaque SIGINT (u : Unit) : UInt32
@[extern "waylean_SIGUSR1"]
opaque SIGUSR1 (u : Unit) : UInt32
@[extern "waylean_SIGUSR2"]
opaque SIGUSR2 (u : Unit) : UInt32
@[extern "waylean_display_new"]
opaque Display.new : (name : @& Option String) → IO Display
@[extern "waylean_display_flush"]
opaque Display.flush : (display : @& Display) → IO Unit
@[extern "waylean_event_loop_new"]
opaque EventLoop.new : IO (EventLoop M)
@[extern "waylean_event_loop_add_display"]
opaque EventLoop.addDisplay : (eventLoop : @& (EventLoop M)) → (display : @& Display) → IO EventSource
@[extern "waylean_event_loop_add_timer"]
opaque EventLoop.addTimer : (eventLoop : @& (EventLoop M)) → (delayMs : UInt32) → (msg : @& M) → IO EventSource
@[extern "waylean_event_loop_add_signal"]
opaque EventLoop.addSignal : (eventLoop : @& (EventLoop M)) → (signum : UInt32) → (msg : @& M) → IO EventSource
@[extern "waylean_event_loop_remove"]
opaque EventLoop.remove : (eventLoop : @& (EventLoop M)) → (source : @& EventSource) → IO Unit
@[extern "waylean_event_loop_quit"]
opaque EventLoop.quit : (eventLoop : @& (EventLoop M)) → IO Unit
@[extern "waylean_event_loop_poll"]
opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M)
@[extern "waylean_type_map_new"]
opaque TypeMap.new : IO TypeMap
@[extern "waylean_type_map_is_complete"]
opaque TypeMap.isComplete : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
@[extern "waylean_type_map_register"]
opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → (setComplete : UInt32) → IO Unit
@[extern "waylean_argument_buffer_new"]
opaque ArgumentBuffer.new : IO ArgumentBuffer
@[extern "waylean_argument_buffer_write_int"]
opaque ArgumentBuffer.writeInt : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit
@[extern "waylean_argument_buffer_write_uint"]
opaque ArgumentBuffer.writeUInt : (writer : @& ArgumentBuffer) → (value : UInt32) → IO Unit
@[extern "waylean_argument_buffer_write_fixed"]
opaque ArgumentBuffer.writeFixed : (writer : @& ArgumentBuffer) → (value : Float32) → IO Unit
@[extern "waylean_argument_buffer_write_string"]
opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @& Option String) → IO Unit
@[extern "waylean_argument_buffer_write_object"]
opaque ArgumentBuffer.writeObject : (writer : @& ArgumentBuffer) → (value : @& Option Proxy) → IO Unit
@[extern "waylean_argument_buffer_write_array"]
opaque ArgumentBuffer.writeArray : (writer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit
@[extern "waylean_argument_buffer_write_fd"]
opaque ArgumentBuffer.writeFD : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit
@[extern "waylean_argument_buffer_read_int"]
opaque ArgumentBuffer.readInt : (reader : @& ArgumentBuffer) → IO Int32
@[extern "waylean_argument_buffer_read_uint"]
opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO UInt32
@[extern "waylean_argument_buffer_read_fixed"]
opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float32
@[extern "waylean_argument_buffer_read_string"]
opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option String)
@[extern "waylean_argument_buffer_read_object"]
opaque ArgumentBuffer.readObject : (reader : @& ArgumentBuffer) → IO (Option Proxy)
@[extern "waylean_argument_buffer_read_array"]
opaque ArgumentBuffer.readArray : (reader : @& ArgumentBuffer) → IO ByteArray
@[extern "waylean_argument_buffer_read_fd"]
opaque ArgumentBuffer.readFD : (reader : @& ArgumentBuffer) → IO Int32
@[extern "waylean_proxy_from_display"]
opaque Proxy.fromDisplay : (display : Display) → IO Proxy
@[extern "waylean_proxy_send"]
opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → IO Unit
@[extern "waylean_proxy_send_constructor"]
opaque Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
@[extern "waylean_proxy_listen"]
opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → EventLoop M × M) → IO Unit
@[extern "waylean_proxy_keep"]
opaque Proxy.keep : (proxy : @& Proxy) → IO Unit
end Wayland.Native
|
