blob: 909cde42e0d1154db3d31511c0ed4db5a9a61635 (
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
143
144
145
|
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 ArgumentReaderP : NonemptyType
private opaque ArgumentWriterP : 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 ArgumentReader : Type := ArgumentReaderP.type
def ArgumentWriter : Type := ArgumentWriterP.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 ArgumentReader := ArgumentReaderP.property
instance : Nonempty ArgumentWriter := ArgumentWriterP.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_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_contains"]
opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
@[extern "waylean_type_map_register"]
opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
@[extern "waylean_argument_writer_new"]
opaque ArgumentWriter.new : IO ArgumentWriter
@[extern "waylean_argument_writer_write_int"]
opaque ArgumentWriter.writeInt : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit
@[extern "waylean_argument_writer_write_uint"]
opaque ArgumentWriter.writeUInt : (writer : @& ArgumentWriter) → (value : UInt32) → IO Unit
@[extern "waylean_argument_writer_write_fixed"]
opaque ArgumentWriter.writeFloat : (writer : @& ArgumentWriter) → (value : Float) → IO Unit
@[extern "waylean_argument_writer_write_string"]
opaque ArgumentWriter.writeString : (writer : @& ArgumentWriter) → (value : @& Option String) → IO Unit
@[extern "waylean_argument_writer_write_object"]
opaque ArgumentWriter.writeObject : (writer : @& ArgumentWriter) → (value : @& Option Proxy) → IO Unit
@[extern "waylean_argument_writer_write_new_id"]
opaque ArgumentWriter.writeNewID : (writer : @& ArgumentWriter) → (value : @& Proxy) → IO Unit
@[extern "waylean_argument_writer_write_array"]
opaque ArgumentWriter.writeArray : (writer : @& ArgumentWriter) → (value : @& ByteArray) → IO Unit
@[extern "waylean_argument_writer_write_fd"]
opaque ArgumentWriter.writeFD : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit
@[extern "waylean_argument_reader_read_int"]
opaque ArgumentReader.readInt : (reader : @& ArgumentReader) → IO Int32
@[extern "waylean_argument_reader_read_uint"]
opaque ArgumentReader.readUInt : (reader : @& ArgumentReader) → IO Int32
@[extern "waylean_argument_reader_read_fixed"]
opaque ArgumentReader.readFixed : (reader : @& ArgumentReader) → IO Float
@[extern "waylean_argument_reader_read_string"]
opaque ArgumentReader.readString : (reader : @& ArgumentReader) → IO (Option String)
@[extern "waylean_argument_reader_read_object"]
opaque ArgumentReader.readObject : (reader : @& ArgumentReader) → IO (Option Proxy)
@[extern "waylean_argument_reader_read_new_id"]
opaque ArgumentReader.readNewID : (reader : @& ArgumentReader) → IO UInt32
@[extern "waylean_argument_reader_read_array"]
opaque ArgumentReader.readArray : (reader : @& ArgumentReader) → IO ByteArray
@[extern "waylean_argument_reader_read_fd"]
opaque ArgumentReader.readFD : (reader : @& ArgumentReader) → IO Int32
@[extern "waylean_proxy_from_display"]
opaque Proxy.fromDisplay : (display : Display) → IO Proxy
@[extern "waylean_proxy_new"]
opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
@[extern "waylean_proxy_send"]
opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit
@[extern "waylean_proxy_listen"]
opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentReader → EventLoop M × M) → IO Unit
end Wayland.Native
|
