From f56f5948391895279540650e26ee2a336be358fd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 11 Apr 2024 22:09:49 +0200
Subject: [PATCH] push multiple loglevel changes at once

---
 lib/Quox/Log.idr | 31 +++++++++++++++++++++----------
 1 file changed, 21 insertions(+), 10 deletions(-)

diff --git a/lib/Quox/Log.idr b/lib/Quox/Log.idr
index faf8385..bfe5d26 100644
--- a/lib/Quox/Log.idr
+++ b/lib/Quox/Log.idr
@@ -138,18 +138,21 @@ mergeLeft l r = foldl (\lst, (k, v) => replace k v lst) r l
 
 
 public export
-data PushArg = SetDefault LogLevel | SetCats LevelMap | SetAll LogLevel
+data PushArg =
+    SetDefault LogLevel
+  | SetCat     LogCategory LogLevel
+  | SetAll     LogLevel
 %name PushArg push
 
 export %inline
-applyPush : PushArg -> LogLevels -> LogLevels
-applyPush (SetDefault def) = {defLevel := def}
-applyPush (SetCats    map) = {levels   $= mergeLeft map}
-applyPush (SetAll     lvl) = const $ MkLogLevels lvl []
+applyPush : LogLevels -> PushArg -> LogLevels
+applyPush lvls (SetDefault def)     = {defLevel := def} lvls
+applyPush lvls (SetCat     cat lvl) = {levels   $= replace cat lvl} lvls
+applyPush lvls (SetAll     lvl)     = MkLogLevels lvl []
 
 export %inline
 fromPush : PushArg -> LogLevels
-fromPush p = applyPush p defaultLogLevels
+fromPush = applyPush defaultLogLevels
 
 
 public export
@@ -167,7 +170,7 @@ data LogL : (lbl : tag) -> Type -> Type where
   SayMany : (cat : LogCategory) -> (loc : Loc) ->
             (msgs : List LogMsg) -> LogL lbl ()
   ||| set some verbosity levels
-  Push : (push : PushArg) -> LogL lbl ()
+  Push : (push : List PushArg) -> LogL lbl ()
   ||| restore the previous verbosity levels.
   ||| returns False if the stack was already empty
   Pop : LogL lbl Bool
@@ -192,9 +195,13 @@ parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
   sayAt cat lvl loc msg = sayManyAt cat loc [lvl :> msg]
 
   public export %inline
-  pushAt : PushArg -> Eff fs ()
+  pushAt : List PushArg -> Eff fs ()
   pushAt lvls = send $ Push {lbl} lvls
 
+  public export %inline
+  push1At : PushArg -> Eff fs ()
+  push1At lvl = pushAt [lvl]
+
   public export %inline
   popAt : Eff fs Bool
   popAt = send $ Pop {lbl}
@@ -216,9 +223,13 @@ parameters {auto _ : Has Log fs}
   say = sayAt ()
 
   public export %inline
-  push : PushArg -> Eff fs ()
+  push : List PushArg -> Eff fs ()
   push = pushAt ()
 
+  public export %inline
+  push1 : PushArg -> Eff fs ()
+  push1 = push1At ()
+
   public export %inline
   pop : Eff fs Bool
   pop = popAt ()
@@ -235,7 +246,7 @@ handleLogSW : (0 s : ts) -> (0 w : tw) ->
               LogL tag a -> Eff fs a
 handleLogSW s w = \case
   Push push => modifyAt s $ \lst =>
-    applyPush push (fromMaybe defaultLogLevels (head' lst)) :: lst
+    foldl applyPush (fromMaybe defaultLogLevels (head' lst)) push :: lst
   Pop => stateAt s $ maybe (False, []) (True,) . tail'
   SayMany cat loc msgs => do
     catLvl <- getsAt s $ fst . getLevel cat