diff options
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index d42147c..2e2ceaa 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -28,7 +28,8 @@ def OpCode : Type := UInt32 deriving Repr, Nonempty, BEq, OfNat /-- Handle to a client object, possibly dead. -/ -def Object (ι : InterfaceName) : Type := Native.Proxy +structure Object (ι : InterfaceName) : Type where + private proxy : Native.Proxy deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ @@ -261,6 +262,19 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter requests := iface'.requestClass.messages.map MessageDesc.toNative events := iface'.eventClass.messages.map MessageDesc.toNative } +/-- Get the `wl_display` instance within the display monad. -/ +def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do + let proxy ← Native.Proxy.fromDisplay (← read).disp + return ⟨proxy⟩ + +/-- Create a new object, allocating a new ID in the client space and inheriting the display from the `factory` +object. -/ +def DisplayM.createObject {ι ι' : InterfaceName} [iface : ResolvedInterface ι] (factory : Object ι') : DisplayM σ (Object ι) := do + ensureInterface ι + let typeMap := (← read).typeMap + let proxy ← Native.Proxy.new factory.proxy typeMap ι + return ⟨proxy⟩ + -- def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry -- def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry |