(id: string, callId: string, now?: number)
| 218 | } |
| 219 | |
| 220 | function endTool(id: string, callId: string, now?: number): number | undefined { |
| 221 | const session = sessions.get(id) |
| 222 | if (!session) return undefined |
| 223 | |
| 224 | const start = session.toolStartTimes.get(callId) |
| 225 | if (start === undefined) return undefined |
| 226 | |
| 227 | session.toolStartTimes.delete(callId) |
| 228 | return (now ?? Date.now()) - start |
| 229 | } |
| 230 | |
| 231 | function size(): number { |
| 232 | return sessions.size |