diff options
Diffstat (limited to 'lib/Wayland')
| -rw-r--r-- | lib/Wayland/Display.lean | 4 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 3 |
2 files changed, 7 insertions, 0 deletions
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) |