From 54d62ad2f3eb72d57683780b55dad2a97b1e2dcb Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 1 Apr 2026 20:51:11 +0200 Subject: clean up demo --- lib/Wayland/Display.lean | 4 ++++ lib/Wayland/Native.lean | 3 +++ 2 files changed, 7 insertions(+) (limited to 'lib/Wayland') diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index f07c5ff..0a049b3 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -317,6 +317,10 @@ def Object.listen {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) ReaderT.run (handler event) global global.listen obj.proxy actualHandler +/-- Shorthand to ensure the reference count of an `Object` does not drop to `0`. -/ +def Object.keep {ι : InterfaceName} (obj : Object ι) : DisplayM σ Unit := + obj.proxy.keep + end Proxies end Wayland diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index dd138e4..f8d4c53 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -136,4 +136,7 @@ opaque Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (arg @[extern "waylean_proxy_listen"] opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → EventLoop M × M) → IO Unit +@[extern "waylean_proxy_keep"] +opaque Proxy.keep : (proxy : @& Proxy) → IO Unit + end Wayland.Native -- cgit v1.3.1