From 6390f8d7e7dfe8c0311cffc2e928e93abb92714b Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 1 Apr 2026 18:23:27 +0200 Subject: try to properly deal with constructors --- lib/Wayland/Native.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'lib/Wayland/Native.lean') diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index 0e8c079..f8943ac 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -94,9 +94,6 @@ opaque ArgumentBuffer.writeString : (writer : @& ArgumentBuffer) → (value : @& @[extern "waylean_argument_buffer_write_object"] opaque ArgumentBuffer.writeObject : (writer : @& ArgumentBuffer) → (value : @& Option Proxy) → IO Unit -@[extern "waylean_argument_buffer_write_new_id"] -opaque ArgumentBuffer.writeNewID : (writer : @& ArgumentBuffer) → (value : @& Proxy) → IO Unit - @[extern "waylean_argument_buffer_write_array"] opaque ArgumentBuffer.writeArray : (writer : @& ArgumentBuffer) → (value : @& ByteArray) → IO Unit @@ -118,9 +115,6 @@ opaque ArgumentBuffer.readString : (reader : @& ArgumentBuffer) → IO (Option S @[extern "waylean_argument_buffer_read_object"] opaque ArgumentBuffer.readObject : (reader : @& ArgumentBuffer) → IO (Option Proxy) -@[extern "waylean_argument_buffer_read_new_id"] -opaque ArgumentBuffer.readNewID : (reader : @& ArgumentBuffer) → IO UInt32 - @[extern "waylean_argument_buffer_read_array"] opaque ArgumentBuffer.readArray : (reader : @& ArgumentBuffer) → IO ByteArray @@ -130,12 +124,12 @@ opaque ArgumentBuffer.readFD : (reader : @& ArgumentBuffer) → 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) → (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 -- cgit v1.3.1