more minor cleanupsHEADmain

1 files changed, 83 insertions, 74 deletions

diff --git a/src/Waylean.lean b/src/Waylean.lean
index 09950ab..138f7c9 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -143,39 +143,73 @@ def Seat.createPointerBinding (mods : RiverSeatV1.Modifiers) (button : UInt32) (
     let pointerBindings := s.pointerBindings.insert proxy { proxy, action }
     set (Option.some { s with pointerBindings })
 
-def Seat.pointerMove {σ : Type} (seat : Seat) (win : Window) : DisplayM σ Seat := do
-  seat.proxy.opStartPointer
-  return { seat with
-    interacted := win.proxy
-    op := .move win.proxy win.x win.y
-    opDeltaX := 0
-    opDeltaY := 0
-  }
+def Seat.pointerMove (win : Window) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    s.proxy.opStartPointer
+    set (Option.some { s with
+      interacted := win.proxy
+      op := .move win.proxy win.x win.y
+      opDeltaX := 0
+      opDeltaY := 0
+    })
+
+def Seat.pointerResize (win : Window) (edges : RiverWindowV1.Edges) : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    s.proxy.opStartPointer
+    win.proxy.informResizeStart
+    set (Option.some { s with
+      interacted := win.proxy
+      op := .resize win.proxy win.x win.y win.width win.height edges
+      opDeltaX := 0
+      opDeltaY := 0
+    })
 
-def Seat.pointerResize {σ : Type} (seat : Seat) (win : Window) (edges : RiverWindowV1.Edges) : DisplayM σ Seat := do
-  seat.proxy.opStartPointer
-  win.proxy.informResizeStart
-  return { seat with
-    interacted := win.proxy
-    op := .resize win.proxy win.x win.y win.width win.height edges
-    opDeltaX := 0
-    opDeltaY := 0
-  }
+def Seat.opEnd : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    match s.op with
+      | .resize proxy _ _ _ _ _ => proxy.informResizeEnd
+      | _ => pure ()
+    s.proxy.opEnd
+    set (Option.some { s with op := .none })
+
+def Seat.opManage : DisplayM (Option Seat) Unit := do
+  for s in ← get do
+    match s.op with
+      | .resize proxy _ _ startWidth startHeight edges =>
+          let mut width := startWidth
+          let mut height := startHeight
+          if edges.left   then width  := width  - s.opDeltaX
+          if edges.right  then width  := width  + s.opDeltaX
+          if edges.top    then height := height - s.opDeltaY
+          if edges.bottom then height := height + s.opDeltaY
+          width  := if width  > 0 then width  else 1
+          height := if height > 0 then height else 1
+          proxy.proposeDimensions width height
+      | _ => pure ()
 
-def Seat.focusTop (s : Seat) : DisplayM State Seat := do
-  let windows := (← get).windowOrder
-  if h : windows.size != 0 then
-    let proxy := windows[windows.size - 1]'(Nat.sub_one_lt (bne_iff_ne.mp h))
-    for win in (← get).windows.get? proxy do
-      s.proxy.focusWindow win.proxy
-      win.node.placeTop
-      return { s with focused := win.proxy }
-  s.proxy.clearFocus
-  return { s with focused := .none }
+def focusTop (seat : RiverSeatV1) : DisplayM State Unit := do
+  let seats ← (← get).seats.modifyM seat fun s ↦ do
+    let order := (← get).windowOrder
+    let windows := (← get).windows
+    let window :=
+      if h : order.size != 0 then
+        windows.get? (order[order.size - 1]'(Nat.sub_one_lt (bne_iff_ne.mp h)))
+      else .none
+    match window with
+      | .some win =>
+          s.proxy.focusWindow win.proxy
+          win.node.placeTop
+          pure { s with focused := win.proxy }
+      | .none =>
+          s.proxy.clearFocus
+          pure { s with focused := .none }
+  set { ← get with seats }
 
-def Seat.doAction (s : Seat) (ctx : Context) : DisplayM State Seat := do
-  let action := s.pendingAction
-  let mut s : Seat := { s with pendingAction := .none }
+def doAction (seat : RiverSeatV1) (ctx : Context) : DisplayM State Unit := do
+  let action ← DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens seat) do
+    match ← get with
+      | .some s => set (Option.some { s with pendingAction := .none }); pure s.pendingAction
+      | .none   => pure .none
   match action with
     | .none =>
         pure ()
@@ -185,7 +219,7 @@ def Seat.doAction (s : Seat) (ctx : Context) : DisplayM State Seat := do
           env := #[("WAYLAND_DEBUG", .none)]
         }
     | .close =>
-        for window in s.focused do
+        for window in (← get).seats.get? seat >>= Seat.focused do
           window.close
     | .focusNext =>
         let mut windowOrder := (← get).windowOrder
@@ -194,37 +228,17 @@ def Seat.doAction (s : Seat) (ctx : Context) : DisplayM State Seat := do
           windowOrder := windowOrder.eraseIdx 0
           windowOrder := windowOrder.push win
         set { ← get with windowOrder }
-        s ← focusTop s
+        focusTop seat
     | .move =>
-        for win in s.hovered >>= (← get).windows.get? do
-          s ← s.pointerMove win
+        for win in (← get).seats.get? seat >>= Seat.hovered >>= (← get).windows.get? do
+          DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens seat) do
+            Seat.pointerMove win
     | .resize =>
-        for win in s.hovered >>= (← get).windows.get? do
-          s ← s.pointerResize win { bottom := true, right := true }
+        for win in (← get).seats.get? seat >>= Seat.hovered >>= (← get).windows.get? do
+          DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens seat) do
+            Seat.pointerResize win { bottom := true, right := true }
     | .exit =>
         ctx.wm.exitSession
-  return s
-
-def Seat.opEnd (s : Seat) : DisplayM State Seat := do
-  match s.op with
-    | .resize proxy _ _ _ _ _ => proxy.informResizeEnd
-    | _ => pure ()
-  s.proxy.opEnd
-  return { s with op := .none }
-
-def Seat.opManage (s : Seat) : DisplayM State Unit := do
-  match s.op with
-    | .resize proxy _ _ startWidth startHeight edges =>
-        let mut width := startWidth
-        let mut height := startHeight
-        if edges.left   then width  := width  - s.opDeltaX
-        if edges.right  then width  := width  + s.opDeltaX
-        if edges.top    then height := height - s.opDeltaY
-        if edges.bottom then height := height + s.opDeltaY
-        width  := if width  > 0 then width  else 1
-        height := if height > 0 then height else 1
-        proxy.proposeDimensions width height
-    | _ => pure ()
 
 def removeOutputs : DisplayM State Unit := do
   let (removedOutputs, aliveOutputs) := (← get).outputs.partition fun _ out ↦ out.removed
@@ -300,12 +314,12 @@ def initNewSeats (ctx : Context) : DisplayM State Unit := do
 
 def manageWindows : DisplayM State Unit := do
   let windows ← (← get).windows.mapM fun _ win ↦ do
-    let mut seats := (← get).seats
     for proxy in win.pointerMoveRequested do
-      seats ← seats.modifyM proxy (fun s ↦ s.pointerMove win)
+      DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens proxy) do
+        Seat.pointerMove win
     for proxy in win.pointerResizeRequested do
-      seats ← seats.modifyM proxy (fun s ↦ s.pointerResize win win.pointerResizeRequestedEdges)
-    set { ← get with seats }
+      DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens proxy) do
+        Seat.pointerResize win win.pointerResizeRequestedEdges
     pure { win with
       pointerMoveRequested := .none
       pointerResizeRequested := .none
@@ -313,7 +327,7 @@ def manageWindows : DisplayM State Unit := do
   set { ← get with windows }
 
 def manageSeats (ctx : Context) : DisplayM State Unit := do
-  let seats ← (← get).seats.mapM fun _ seat ↦ do
+  for seat in (← get).seats.values do
     for proxy in seat.interacted do
       let mut windowOrder := (← get).windowOrder
       let winIdx := windowOrder.findIdx (· == proxy)
@@ -322,17 +336,12 @@ def manageSeats (ctx : Context) : DisplayM State Unit := do
         windowOrder := windowOrder.eraseIdx winIdx
         windowOrder := windowOrder.push win
       set { ← get with windowOrder }
-    let mut seat := seat
-    seat ← seat.focusTop
-    seat ← seat.doAction ctx
-    if seat.opRelease then
-      seat ← seat.opEnd
-    else
-      seat.opManage
-    pure { seat with
-      interacted := .none
-      opRelease := false
-    }
+    focusTop seat.proxy
+    doAction seat.proxy ctx
+    DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens seat.proxy) do
+      if seat.opRelease then Seat.opEnd
+      else Seat.opManage
+  let seats := (← get).seats.map fun _ s ↦ { s with interacted := .none, opRelease := false }
   set { ← get with seats }
 
 def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit