diff options
Diffstat (limited to 'src/Waylean.lean')
| -rw-r--r-- | src/Waylean.lean | 25 |
1 files changed, 9 insertions, 16 deletions
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 := |