diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2026-04-04 00:06:40 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2026-04-04 00:06:40 +0200 |
| commit | 9d537c6a480bbb8835aaae5c8a5918004442c3c6 (patch) | |
| tree | 566185491ae6dfa53ce3af681431d0729149e161 /lib/Wayland | |
| parent | 4119fa8c0c59bb39f9aeba7f479067fd834c4e20 (diff) | |
referenced interfaces
Diffstat (limited to 'lib/Wayland')
| -rw-r--r-- | lib/Wayland/Display.lean | 5 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 6 |
2 files changed, 6 insertions, 5 deletions
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 diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index f8d4c53..430472b 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -73,11 +73,11 @@ opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M) @[extern "waylean_type_map_new"] opaque TypeMap.new : IO TypeMap -@[extern "waylean_type_map_contains"] -opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool +@[extern "waylean_type_map_is_complete"] +opaque TypeMap.isComplete : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool @[extern "waylean_type_map_register"] -opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit +opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → (setComplete : UInt32) → IO Unit @[extern "waylean_argument_buffer_new"] opaque ArgumentBuffer.new : IO ArgumentBuffer |