From 658b74715751cb4b52b2a968325ece9a62a29fc3 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Sun, 8 Mar 2026 17:27:51 +0100
Subject: display monad

---
 src/Waylean.lean | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'src/Waylean.lean')

diff --git a/src/Waylean.lean b/src/Waylean.lean
index a13b867..354b609 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,21 +1,21 @@
 import Wayland
-open Wayland.Native
+open Wayland
 
-partial def mainLoop (loop : EventLoop (IO Unit)) : IO Unit := do
-  match (← loop.poll) with
-  | .none => return
-  | .some msg => msg; mainLoop loop
+structure State where
+  count : Int
 
-partial def main : IO Unit := do
-  let disp : Display ← Display.new .none
-  let loop : EventLoop (IO Unit) ← EventLoop.new
-  _ ← loop.addDisplay disp
-  _ ← loop.addSignal SIGINT (do
-    IO.println "Received SIGINT"
-    loop.quit)
-  let rec setUpTimer := loop.addTimer 500 (do
-    IO.println "Timer tick"
-    _ ← setUpTimer)
-  _ ← setUpTimer
-  disp.roundtrip
-  mainLoop loop
+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 launch : DisplayM State Unit := do
+  _ ← DisplayM.registerSignal .SIGINT do
+    DisplayM.liftIO (IO.println "Received SIGINT")
+    DisplayM.requestQuit
+  DisplayM.zoom (mk_lens count) nextTimer
+
+def main : IO Unit :=
+  DisplayM.run launch { count := 0 }
-- 
cgit v1.3.1