diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2026-03-13 20:49:22 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2026-03-13 20:49:22 +0100 |
| commit | 0b7ad07db1be69f75ca9b469fd6210c64ba87dd5 (patch) | |
| tree | fbdd654ce723d60972d8d6a6f7aca668fe921ab9 /lib/Wayland/Native.lean | |
| parent | ad2c02141844d48e9c50a05f5ce872db283751ce (diff) | |
outline proxy api
Diffstat (limited to 'lib/Wayland/Native.lean')
| -rw-r--r-- | lib/Wayland/Native.lean | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index e695e5f..f889c25 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -17,16 +17,25 @@ private opaque DisplayP : NonemptyType private opaque EventLoopP (M : Type) : NonemptyType private opaque EventSourceP : NonemptyType private opaque TypeMapP : NonemptyType +private opaque ProxyP : NonemptyType +private opaque ArgumentReaderP : NonemptyType +private opaque ArgumentWriterP : 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 Proxy : Type := ProxyP.type +def ArgumentReader : Type := ArgumentReaderP.type +def ArgumentWriter : Type := ArgumentWriterP.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 Proxy := ProxyP.property +instance : Nonempty ArgumentReader := ArgumentReaderP.property +instance : Nonempty ArgumentWriter := ArgumentWriterP.property @[extern "waylean_SIGINT"] opaque SIGINT (u : Unit) : UInt32 @@ -73,4 +82,16 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → @[extern "waylean_type_map_register"] opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit +@[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 |