summaryrefslogtreecommitdiff
path: root/src/Waylean.lean
diff options
context:
space:
mode:
Diffstat (limited to 'src/Waylean.lean')
-rw-r--r--src/Waylean.lean35
1 files changed, 31 insertions, 4 deletions
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 47f9db9..8402351 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,23 +1,50 @@
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.liftIO <| IO.println "Received SIGINT"
DisplayM.requestQuit
-
zoomRegistry Registry.init
DisplayM.sync do
- let shm : WlShm ← zoomRegistry Registry.bindSingleton
- shm.release
+ let wm : RiverWindowManagerV1 ← zoomRegistry Registry.bindSingleton
+ let xkbBindings : RiverXkbBindingsV1 ← zoomRegistry Registry.bindSingleton
+ wm.listen (handle { wm, xkbBindings })
def main : IO Unit :=
DisplayM.run launch { }