diff options
Diffstat (limited to 'src/Waylean.lean')
| -rw-r--r-- | src/Waylean.lean | 36 |
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 { } |
