From 265fd38f34326ced72fe4684d61418125c7cde9c Mon Sep 17 00:00:00 2001
From: James Sully <sullyj3@gmail.com>
Date: Sat, 3 Aug 2024 17:31:15 +1000
Subject: [PATCH] Display id of created timer (closes #29)

---
 src/Sand/Message.lean    | 2 +-
 src/Sand/SandClient.lean | 4 ++--
 src/Sand/SandDaemon.lean | 7 ++++---
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/Sand/Message.lean b/src/Sand/Message.lean
index d2a65a4..0da4309 100644
--- a/src/Sand/Message.lean
+++ b/src/Sand/Message.lean
@@ -16,7 +16,7 @@ inductive Command
 
 -- responses to commands sent from server to client
 inductive AddTimerResponse
-  | ok
+  | ok (createdId : TimerId)
   deriving Repr, ToJson, FromJson
 
 inductive ListResponse
diff --git a/src/Sand/SandClient.lean b/src/Sand/SandClient.lean
index ab3e1ea..523cd67 100644
--- a/src/Sand/SandClient.lean
+++ b/src/Sand/SandClient.lean
@@ -171,8 +171,8 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
   -- Handle response
   match cmd with
   | Command.addTimer timer => do
-    let .ok := resp
-    println! "Timer created for {timer.formatColonSeparated}."
+    let .ok id := resp
+    println! "Timer #{repr id.id} created for {timer.formatColonSeparated}."
   | Command.cancelTimer timerId => match resp with
     | .ok =>
       println! "Timer #{repr timerId.id} cancelled."
diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean
index ff2d441..e98e6b7 100644
--- a/src/Sand/SandDaemon.lean
+++ b/src/Sand/SandDaemon.lean
@@ -143,7 +143,7 @@ def DaemonState.initial : IO DaemonState := do
     timers := (← IO.Mutex.new ∅)
   }
 
-def addTimer (duration : Duration) : CmdHandlerT IO Unit := do
+def addTimer (duration : Duration) : CmdHandlerT IO TimerId := do
   let {clientConnectedTime, state, ..} ← read
 
   let msg := s!"Starting timer for {duration.formatColonSeparated}"
@@ -160,13 +160,14 @@ def addTimer (duration : Duration) : CmdHandlerT IO Unit := do
   let countdownTask ← (countdown id due).asTask .dedicated
 
   state.timers.atomically <| modify (·.insert id (timer, .running countdownTask))
+  return id
 
 def handleClientCmd (cmd : Command) : CmdHandlerT IO (ResponseFor cmd) := do
   let {state, ..} ← read
   match cmd with
   | .addTimer duration => do
-    addTimer duration
-    return .ok
+    let id ← addTimer duration
+    return .ok id
   | .cancelTimer which => removeTimer which
   | .list => do
     let timers ← state.timers.atomically get