Web: hide notifications after a few seconds

The notifications (like "job requeued" after pushing the "requeue" button)
are now hidden after 5 seconds.

web/app/src/stores/notifications.js

@@ -1,5 +1,8 @@
 import { defineStore } from 'pinia'
 
+/** Time after which a notification is hidden. */
+const MESSAGE_HIDE_DELAY_MS = 5000;
+
 /**
  * Store notifications to users of the web frontend.
  */
@@ -8,7 +11,9 @@ export const useNotifs = defineStore('notifications', {
     /** @type {{ msg: string, time: Date }[]} */
     history: [],
     /** @type { msg: string, time: Date } */
-    last: null,
+    last: "",
+
+    hideTimerID: 0,
   }),
   actions: {
     /**
@@ -20,6 +25,7 @@ export const useNotifs = defineStore('notifications', {
       this.history.push(notif);
       this.last = notif;
       this._prune();
+      this._restartHideTimer();
     },
 
     /* Ensure there is only 1000 items in the history. */
@@ -27,5 +33,16 @@ export const useNotifs = defineStore('notifications', {
       if (this.history.length <= 1000) return;
       this.history.splice(0, 1000 - this.history.length);
     },
+
+    _restartHideTimer() {
+      if (this.hideTimerID) window.clearTimeout(this.hideTimerID);
+      this.hideTimerID = window.setTimeout(this._hideMessage, MESSAGE_HIDE_DELAY_MS);
+    },
+    _hideMessage() {
+      this.$patch({
+        hideTimerID: 0,
+        last: "",
+      });
+    },
   },
 })