Display id of created timer (closes #29)

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

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."

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