diff options
Diffstat (limited to 'lib/Wayland')
| -rw-r--r-- | lib/Wayland/Native.lean | 81 |
1 files changed, 39 insertions, 42 deletions
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index 909cde4..9eb8398 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -17,24 +17,21 @@ 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 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 ArgumentReader : Type := ArgumentReaderP.type -def ArgumentWriter : Type := ArgumentWriterP.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 ArgumentReader := ArgumentReaderP.property -instance : Nonempty ArgumentWriter := ArgumentWriterP.property +instance : Nonempty ArgumentBuffer := ArgumentBufferP.property instance : Nonempty Proxy := ProxyP.property @[extern "waylean_SIGINT"] @@ -79,56 +76,56 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → @[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_buffer_new"] +opaque ArgumentBuffer.new : IO ArgumentBuffer -@[extern "waylean_argument_writer_write_int"] -opaque ArgumentWriter.writeInt : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit +@[extern "waylean_argument_buffer_write_int"] +opaque ArgumentBuffer.writeInt : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit -@[extern "waylean_argument_writer_write_uint"] -opaque ArgumentWriter.writeUInt : (writer : @& ArgumentWriter) → (value : UInt32) → IO Unit +@[extern "waylean_argument_buffer_write_uint"] +opaque ArgumentBuffer.writeUInt : (writer : @& ArgumentBuffer) → (value : UInt32) → IO Unit -@[extern "waylean_argument_writer_write_fixed"] -opaque ArgumentWriter.writeFloat : (writer : @& ArgumentWriter) → (value : Float) → IO Unit +@[extern "waylean_argument_buffer_write_fixed"] +opaque ArgumentBuffer.writeFloat : (writer : @& ArgumentBuffer) → (value : Float) → IO Unit -@[extern "waylean_argument_writer_write_string"] -opaque ArgumentWriter.writeString : (writer : @& ArgumentWriter) → (value : @& Option String) → IO Unit +@[extern "waylean_argument_buffer_write_string"] +opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @& Option String) → IO Unit -@[extern "waylean_argument_writer_write_object"] -opaque ArgumentWriter.writeObject : (writer : @& ArgumentWriter) → (value : @& Option Proxy) → IO Unit +@[extern "waylean_argument_buffer_write_object"] +opaque ArgumentBuffer.writeObject : (writer : @& ArgumentBuffer) → (value : @& Option Proxy) → IO Unit -@[extern "waylean_argument_writer_write_new_id"] -opaque ArgumentWriter.writeNewID : (writer : @& ArgumentWriter) → (value : @& Proxy) → IO Unit +@[extern "waylean_argument_buffer_write_new_id"] +opaque ArgumentBuffer.writeNewID : (writer : @& ArgumentBuffer) → (value : @& Proxy) → IO Unit -@[extern "waylean_argument_writer_write_array"] -opaque ArgumentWriter.writeArray : (writer : @& ArgumentWriter) → (value : @& ByteArray) → IO Unit +@[extern "waylean_argument_buffer_write_array"] +opaque ArgumentBuffer.writeArray : (writer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit -@[extern "waylean_argument_writer_write_fd"] -opaque ArgumentWriter.writeFD : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit +@[extern "waylean_argument_buffer_write_fd"] +opaque ArgumentBuffer.writeFD : (writer : @& ArgumentBuffer) → (value : Int32) → IO Unit -@[extern "waylean_argument_reader_read_int"] -opaque ArgumentReader.readInt : (reader : @& ArgumentReader) → IO Int32 +@[extern "waylean_argument_buffer_read_int"] +opaque ArgumentBuffer.readInt : (reader : @& ArgumentBuffer) → IO Int32 -@[extern "waylean_argument_reader_read_uint"] -opaque ArgumentReader.readUInt : (reader : @& ArgumentReader) → IO Int32 +@[extern "waylean_argument_buffer_read_uint"] +opaque ArgumentBuffer.readUInt : (reader : @& ArgumentBuffer) → IO Int32 -@[extern "waylean_argument_reader_read_fixed"] -opaque ArgumentReader.readFixed : (reader : @& ArgumentReader) → IO Float +@[extern "waylean_argument_buffer_read_fixed"] +opaque ArgumentBuffer.readFixed : (reader : @& ArgumentBuffer) → IO Float -@[extern "waylean_argument_reader_read_string"] -opaque ArgumentReader.readString : (reader : @& ArgumentReader) → IO (Option String) +@[extern "waylean_argument_buffer_read_string"] +opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option String) -@[extern "waylean_argument_reader_read_object"] -opaque ArgumentReader.readObject : (reader : @& ArgumentReader) → IO (Option Proxy) +@[extern "waylean_argument_buffer_read_object"] +opaque ArgumentBuffer.readObject : (reader : @& ArgumentBuffer) → IO (Option Proxy) -@[extern "waylean_argument_reader_read_new_id"] -opaque ArgumentReader.readNewID : (reader : @& ArgumentReader) → IO UInt32 +@[extern "waylean_argument_buffer_read_new_id"] +opaque ArgumentBuffer.readNewID : (reader : @& ArgumentBuffer) → IO UInt32 -@[extern "waylean_argument_reader_read_array"] -opaque ArgumentReader.readArray : (reader : @& ArgumentReader) → IO ByteArray +@[extern "waylean_argument_buffer_read_array"] +opaque ArgumentBuffer.readArray : (reader : @& ArgumentBuffer) → IO ByteArray -@[extern "waylean_argument_reader_read_fd"] -opaque ArgumentReader.readFD : (reader : @& ArgumentReader) → IO Int32 +@[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 @@ -137,9 +134,9 @@ opaque Proxy.fromDisplay : (display : Display) → IO Proxy 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 +opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → IO Unit @[extern "waylean_proxy_listen"] -opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentReader → EventLoop M × M) → IO Unit +opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → EventLoop M × M) → IO Unit end Wayland.Native |