diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2026-04-01 20:37:48 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2026-04-01 20:37:48 +0200 |
| commit | f2272d4210f80731a200a1a4d41fa1a29e1d2074 (patch) | |
| tree | 63cd8fc5cf54985a905dfbd2bf63d4bd36b4d493 /lib/Wayland/Display.lean | |
| parent | 6390f8d7e7dfe8c0311cffc2e928e93abb92714b (diff) | |
fix demo
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 4 |
1 files changed, 4 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. -/ |