From f4cff95f32c523ee794427d06740fe3eaca76421 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Fri, 5 Jun 2026 23:36:58 +0200
Subject: lens composition

---
 src/Waylean.lean | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

(limited to 'src/Waylean.lean')

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
-- 
cgit v1.3.1