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