summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Waylean.lean36
1 files changed, 17 insertions, 19 deletions
diff --git a/src/Waylean.lean b/src/Waylean.lean
index f7eb668..953096a 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,32 +1,30 @@
import Wayland
-open Wayland Protocols
-def Wayland.Protocols.WlDisplay.roundtrip {σ : Type} (display : WlDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
- let callback ← display.sync
- callback.listen fun
- | .done _ => do
- callback.keep
- handler
+open Wayland Protocols
structure State where
- count : Int
+ shmName : Option UInt32 := .none
-partial def nextTimer : DisplayM Int Unit := do
- _ ← DisplayM.registerTimer 16ms do
- let newCount := (← get) + 1
- set newCount
- DisplayM.liftIO (IO.println s!"Timer tick {newCount}")
- nextTimer
+def requireGlobal (name : String) : Option UInt32 → DisplayM State UInt32
+ | .some global => pure global
+ | .none => DisplayM.liftIO <| throw (.userError s!"Missing required global {name}")
def launch : DisplayM State Unit := do
_ ← DisplayM.registerSignal .SIGINT do
DisplayM.liftIO (IO.println "Received SIGINT")
DisplayM.requestQuit
- DisplayM.zoom (mk_lens count) nextTimer
-
- let disp : WlDisplay ← DisplayM.getDisplay
- disp.roundtrip do
+ let disp ← DisplayM.getDisplay
+ let registry ← disp.getRegistry
+ registry.listen fun
+ | .global name "wl_shm" _ => do
+ DisplayM.liftIO (IO.println s!"shm global registerd ({name})")
+ set ({ shmName := name } : State)
+ | _ => pure ()
+ disp.sync do
DisplayM.liftIO (IO.println "Roundtrip complete")
+ let shmName ← (← get).shmName |> requireGlobal "wl_shm"
+ let shm : WlShm ← registry.bind shmName
+ shm.release
def main : IO Unit :=
- DisplayM.run launch { count := 0 }
+ DisplayM.run launch { }