blob: 71d02d56f0053e0a7298632942c65327af824a7f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
import Wayland.Display
import Wayland.Protocols
-- Helpers that depend on the protocols and can thus not be included in `Display.lean`.
namespace Wayland
open Protocols
variable {σ : Type}
/-- Get the `wl_display` instance within the display monad. -/
def DisplayM.getDisplay : DisplayM σ WlDisplay := getDisplay'
def DisplayM.sync (done : DisplayM σ Unit) : DisplayM σ Unit := do
(← getDisplay).sync done
def DisplayM.getRegistry : DisplayM σ WlRegistry := do
(← getDisplay).getRegistry
end Wayland
|
