From 9d537c6a480bbb8835aaae5c8a5918004442c3c6 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sat, 4 Apr 2026 00:06:40 +0200 Subject: referenced interfaces --- lib/Wayland/Display.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'lib/Wayland/Display.lean') diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 0a049b3..7bf55c5 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -281,13 +281,14 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message := /-- Ensure the given interface (and all of its dependencies) are registered in the display's `TypeMap`. -/ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInterface ι] : DisplayM σ Unit := do let typeMap := (← read).typeMap - for ⟨ι', iface'⟩ in iface.referencedInterfaces do - if !(← typeMap.contains ι') then + if not (← typeMap.isComplete ι) then + for ⟨ι', iface'⟩ in iface.referencedInterfaces do typeMap.register { name := ι' version := iface'.version requests := iface'.requests.map MessageDesc.toNative events := iface'.events.map MessageDesc.toNative } + (setComplete := if ι' == ι then 1 else 0) /-- Get the `wl_display` instance within the display monad. -/ def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do -- cgit v1.3.1