pause/resume (WIP)

sullyj3 · Jul 28, 2024 · 92f30b6 · 92f30b6
1 parent 358daf3
commit 92f30b6
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 0 deletions.
diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean
@@ -90,6 +90,8 @@ inductive Command
  | addTimer (duration : Duration)
  | list
  | cancelTimer (which : TimerId)
+ | pause (which : TimerId)
+ | resume (which : TimerId)
  deriving Repr, ToJson, FromJson
 
 -- responses to commands sent from server to client

diff --git a/src/Sand/SandClient.lean b/src/Sand/SandClient.lean
@@ -173,6 +173,8 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
  let .list timers := resp | unexpectedResponse respStr
  let now ← IO.monoMsNow
  IO.println <| showTimers timers.data now
+ | Command.pause which => sorry
+ | Command.resume which => sorry
 
  where
  unexpectedResponse {α : Type} (resp : String) : IO α := do

diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean
@@ -29,11 +29,18 @@ def addTimer (state : SanddState) (due : Nat) : BaseIO TimerId := do
  state.timers.atomically <| modify (·.insert id timer)
  return id
 
+
 inductive TimerOpError
  | notFound
 
 def TimerOpResult α := Except TimerOpError α
 
+def pauseTimer (state : SanddState) (timerId : TimerId)
+ : BaseIO (TimerOpResult Unit) := sorry
+
+def resumeTimer (state : SanddState) (timerId : TimerId)
+ : BaseIO (TimerOpResult Unit) := sorry
+
 def removeTimer (state : SanddState) (id : TimerId) : BaseIO (TimerOpResult Unit) := do
  let timers ← state.timers.atomically get
  -- match timers.findIdx? (λ timer ↦ timer.id == id) with
@@ -128,6 +135,8 @@ def handleClientCmd
  | .list => do
  let timers ← state.timers.atomically get
  _ ← client.send <| (CmdResponse.list timers.values).serialize
+ | .pause which => sorry
+ | .resume which => sorry
 
 def handleClient
  (client : Socket)