Related to #441

• Embed Spectacle inside the VS Code extension via the tlaSpectacle.open command and a CSP-safe webview that injects the active editor’s spec into the bundled UI while staying fully offline.
• Add tools/fetch-spectacle.js, a deterministic bundling script that clones Spectacle, whitelists essential assets, vendors JetBrains Mono & Source Code Pro fonts, strips analytics/external fonts, rewrites worker/resource paths, injects a history guard plus router-disable flag, implements TLC Assert, and emits a SHA256 manifest so reruns reproduce the bundle exactly.
• Trim the shipped payload to ~9.4 MB by pruning bootstrap icons, animation demos, and other optional assets; animation remains intentionally omitted to stay within marketplace and offline constraints.
• Extend coverage with a unit test for buildSpectacleHtml and Playwright smoke tests that serve the bundle over an internal HTTP server, stub acquireVsCodeApi, verify Spectacle renders, and run a PlusCal trace (squares.tla) to prove the injected Assert works.

Key Decisions

1. Offline-first fetch script: automate all asset pruning/patching so the bundle stays deterministic, offline, and size-capped whenever Spectacle is refreshed.
2. History/router shim: VS Code webviews block history.replaceState/pushState, so Spectacle now guards those calls and can run with a router-disable mode.
3. Animation exclusion: optional animation demos pull remote assets and add weight; removing them keeps the extension lean and compliant while still covering core spec exploration.
4. Testing: combine Mocha HTML tests with new Playwright smoke tests to ensure the trimmed bundle loads through VS Code messaging and evaluates PlusCal specs without errors.