blob: 63343014f6944fbb352ca386bed4731d8900703d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
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
IO.println "Finished"
DisplayM.requestQuit
| .manageStart => do
IO.println "Manage Start"
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 fun ev ↦ do
wm.keep
xkbBindings.keep
handle { wm, xkbBindings } ev
def main : IO Unit :=
DisplayM.run launch { } (name := "wayland-2")
|
