fix generic new_ids

1 files changed, 17 insertions, 19 deletions

diff --git a/src/Waylean.lean b/src/Waylean.lean
index f7eb668..953096a 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,32 +1,30 @@
 import Wayland
-open Wayland Protocols
 
-def Wayland.Protocols.WlDisplay.roundtrip {σ : Type} (display : WlDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
-  let callback ← display.sync
-  callback.listen fun
-    | .done _ => do
-      callback.keep
-      handler
+open Wayland Protocols
 
 structure State where
-  count : Int
+  shmName : Option UInt32 := .none
 
-partial def nextTimer : DisplayM Int Unit := do
-  _ ← DisplayM.registerTimer 16ms do
-    let newCount := (← get) + 1
-    set newCount
-    DisplayM.liftIO (IO.println s!"Timer tick {newCount}")
-    nextTimer
+def requireGlobal (name : String) : Option UInt32 → DisplayM State UInt32
+  | .some global => pure global
+  | .none        => DisplayM.liftIO <| throw (.userError s!"Missing required global {name}")
 
 def launch : DisplayM State Unit := do
   _ ← DisplayM.registerSignal .SIGINT do
     DisplayM.liftIO (IO.println "Received SIGINT")
     DisplayM.requestQuit
-  DisplayM.zoom (mk_lens count) nextTimer
-
-  let disp : WlDisplay ← DisplayM.getDisplay
-  disp.roundtrip do
+  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
+    shm.release
 
 def main : IO Unit :=
-  DisplayM.run launch { count := 0 }
+  DisplayM.run launch { }