diff options
Diffstat (limited to 'src/Waylean.lean')
| -rw-r--r-- | src/Waylean.lean | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/src/Waylean.lean b/src/Waylean.lean index e47c6ad..dd43179 100644 --- a/src/Waylean.lean +++ b/src/Waylean.lean @@ -308,15 +308,14 @@ def initNewSeats (ctx : Context) : DisplayM State Unit := do let mods : RiverSeatV1.Modifiers := { mod1 := true } for s in (← get).seats.values.filter Seat.new do - DisplayM.zoom (mk_lens seats) do - DisplayM.zoom (Std.HashMap.lens s.proxy) do - set (Option.some { s with new := false }) - Seat.createXkbBinding ctx mods space .spawnFoot - Seat.createXkbBinding ctx mods q .close - Seat.createXkbBinding ctx mods n .focusNext - Seat.createXkbBinding ctx mods esc .exit - Seat.createPointerBinding mods btnLeft .move - Seat.createPointerBinding mods btnRight .resize + DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens s.proxy) do + set (Option.some { s with new := false }) + Seat.createXkbBinding ctx mods space .spawnFoot + Seat.createXkbBinding ctx mods q .close + Seat.createXkbBinding ctx mods n .focusNext + Seat.createXkbBinding ctx mods esc .exit + Seat.createPointerBinding mods btnLeft .move + Seat.createPointerBinding mods btnRight .resize def manageWindows : DisplayM State Unit := do let windows ← (← get).windows.mapM fun win ↦ do @@ -400,15 +399,13 @@ def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit | .output proxy => do let outputs := (← get).outputs.insert proxy { proxy } set { ← get with outputs } - DisplayM.zoom (mk_lens outputs) do - DisplayM.zoom (Std.HashMap.lens proxy) do - proxy.listen handleOutput + DisplayM.zoom (mk_lens outputs ≫ Std.HashMap.lens proxy) do + proxy.listen handleOutput | .seat proxy => do let seats := (← get).seats.insert proxy { proxy } set { ← get with seats } - DisplayM.zoom (mk_lens seats) do - DisplayM.zoom (Std.HashMap.lens proxy) do - proxy.listen handleSeat + DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens proxy) do + proxy.listen handleSeat def launch : DisplayM State Unit := do _ ← DisplayM.registerSignal .SIGINT do |
