diff options
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 |