import Wayland import Waylean.Registry import Std.Data.HashMap open Wayland Protocols Waylean structure Output where removed : Bool structure State where registry : Registry.State := .new outputs : Std.HashMap RiverOutputV1 Output := { } structure Context where wm : RiverWindowManagerV1 xkbBindings : RiverXkbBindingsV1 abbrev WindowManagerM (σ : Type) := ReaderT Context (DisplayM σ) def zoomRegistry {α : Type} : DisplayM Registry.State α → DisplayM State α := DisplayM.zoom (mk_lens registry) def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit | .unavailable => do DisplayM.liftIO <| IO.println "Another window manager is already running" DisplayM.requestQuit | .finished => do DisplayM.requestQuit | .manageStart => do let (removedOutputs, aliveOutputs) := (← get).outputs.partition (Function.const _ Output.removed) pure () | .renderStart => pure () | .sessionLocked => pure () | .sessionUnlocked => pure () | .window win => pure () | .output out => pure () | .seat seat => pure () def launch : DisplayM State Unit := do _ ← DisplayM.registerSignal .SIGINT do DisplayM.liftIO <| IO.println "Received SIGINT" DisplayM.requestQuit zoomRegistry Registry.init DisplayM.sync do let wm : RiverWindowManagerV1 ← zoomRegistry Registry.bindSingleton let xkbBindings : RiverXkbBindingsV1 ← zoomRegistry Registry.bindSingleton wm.listen (handle { wm, xkbBindings }) def main : IO Unit := DisplayM.run launch { }