Give the coordinator working crew management tools

- Resolve the crew and workspaces fresh inside each tool run, so a bot or
  workspace created earlier in the same reply is usable: create_bot,
  assign_computer, add_bot_to_workspace, delegate_task and
  set_bot_workspace_instructions.
- Add coordinator-only update_bot, find_bot, find_workspace, delete_bot,
  delete_workspace and remove_bot_from_workspace tools.
- Push server:workspace-removed when a workspace is deleted, and
  workspace_ids on server:bot-updated so a workspace's crew drops a bot
  that was taken out of it.

src/bots-queue/push-bot-updated.ts

@@ -19,6 +19,11 @@ type Params = {
      * live relay). Null means its main one.
      */
     computer_id?: number | null;
+    /**
+     * The workspaces the bot is in now, for a membership change: a
+     * workspace's crew drops a bot that's no longer in it.
+     */
+    workspace_ids?: number[];
 };
 
 /**
@@ -26,7 +31,13 @@ type Params = {
  * (`grabBotAudience`), each with their own face, status line and active
  * task with it, never another user's.
  */
-export default async function pushBotUpdated({ bot_id, user_id, users, computer_id }: Params) {
+export default async function pushBotUpdated({
+    bot_id,
+    user_id,
+    users,
+    computer_id,
+    workspace_ids,
+}: Params) {
     if (!bot_id) return;
 
     const audience = user_id ? [user_id] : await grabBotAudience({ bot_id });
@@ -42,6 +53,7 @@ export default async function pushBotUpdated({ bot_id, user_id, users, computer_
                     id: Number(bot_id),
                     ...(await grabBotFace({ bot_id, user_id: viewer_id })),
                     ...(computer_id !== undefined ? { computer_id: computer_id || null } : {}),
+                    ...(workspace_ids !== undefined ? { workspace_ids } : {}),
                     task: await grabActiveBotTask({ bot_id, user_id: viewer_id }),
                 },
             },

src/bots-queue/push-workspace-removed.ts

@@ -0,0 +1,28 @@
+import { sendToUser } from "@/src/websocket/(functions)/send-to-user";
+
+type Params = {
+    workspace_id: number | string;
+    /**
+     * Everyone who saw the workspace, read before its row was deleted:
+     * afterwards its links are gone with it, so its audience can't be
+     * worked out any more.
+     */
+    user_ids: number[];
+};
+
+/**
+ * Pushes `server:workspace-removed` to everyone who could see a workspace
+ * that was deleted, so its rail row goes at once and nothing opens a dead
+ * workspace.
+ */
+export default function pushWorkspaceRemoved({ workspace_id, user_ids }: Params) {
+    for (const user_id of user_ids) {
+        sendToUser({
+            user_id,
+            data: {
+                event: "server:workspace-removed",
+                data: { workspace_id: Number(workspace_id) },
+            },
+        });
+    }
+}