From f2272d4210f80731a200a1a4d41fa1a29e1d2074 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 1 Apr 2026 20:37:48 +0200 Subject: fix 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 5747c4d..f07c5ff 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -166,6 +166,10 @@ not be used often. -/ def DisplayM.liftIO (io : IO α) : DisplayM σ α := io +/-- Flush any pending requests. -/ +def DisplayM.flush : DisplayM σ Unit := do + (← read).disp.flush + /-- Request the application to stop processing events and exit the event loop. This can be sent at any time and stops the event loop before any further events can be processed. -/ diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index f8943ac..dd138e4 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -46,6 +46,9 @@ opaque SIGUSR2 (u : Unit) : UInt32 @[extern "waylean_display_new"] opaque Display.new : (name : @& Option String) → IO Display +@[extern "waylean_display_flush"] +opaque Display.flush : (display : @& Display) → IO Unit + @[extern "waylean_event_loop_new"] opaque EventLoop.new : IO (EventLoop M) -- cgit v1.3.1