From dab858e92dfa5705d1aef7259e03b25747372d95 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Fri, 10 Apr 2026 17:36:15 +0200
Subject: implement registry wrapper

---
 src/Waylean.lean | 25 +++++++++----------------
 1 file changed, 9 insertions(+), 16 deletions(-)

(limited to 'src/Waylean.lean')

diff --git a/src/Waylean.lean b/src/Waylean.lean
index 953096a..47f9db9 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,29 +1,22 @@
 import Wayland
+import Waylean.Registry
 
-open Wayland Protocols
+open Wayland Protocols Waylean
 
 structure State where
-  shmName : Option UInt32 := .none
+  registry : Registry.State := .new
 
-def requireGlobal (name : String) : Option UInt32 → DisplayM State UInt32
-  | .some global => pure global
-  | .none        => DisplayM.liftIO <| throw (.userError s!"Missing required global {name}")
+def zoomRegistry {α : Type} : DisplayM Registry.State α → DisplayM State α :=
+  DisplayM.zoom (mk_lens registry)
 
 def launch : DisplayM State Unit := do
   _ ← DisplayM.registerSignal .SIGINT do
     DisplayM.liftIO (IO.println "Received SIGINT")
     DisplayM.requestQuit
-  let disp ← DisplayM.getDisplay
-  let registry ← disp.getRegistry
-  registry.listen fun
-    | .global name "wl_shm" _ => do
-        DisplayM.liftIO (IO.println s!"shm global registerd ({name})")
-        set ({ shmName := name } : State)
-    | _ => pure ()
-  disp.sync do
-    DisplayM.liftIO (IO.println "Roundtrip complete")
-    let shmName ← (← get).shmName |> requireGlobal "wl_shm"
-    let shm : WlShm ← registry.bind shmName
+
+  zoomRegistry Registry.init
+  DisplayM.sync do
+    let shm : WlShm ← zoomRegistry Registry.bindSingleton
     shm.release
 
 def main : IO Unit :=
-- 
cgit v1.3.1