As a side note, VSCode has a couple of handy features that might be useful for Metamath users:
1. **Yamma and the Problems Tab** When using Yamma, it might be helpful to keep the **Problems tab** open. By default, the tab shows all warnings and errors across your entire workspace, which can be useful if you’re working with multiple `.mmp`, `.mm`, or `.mmt` files. Files with issues are also highlighted in the left navigation bar with small numbers, making it easy to identify "problematic" files. However, if you want to focus on a single file, you can enable the **"Show active file only"** filter in the Problems tab. This will display only the diagnostics for the `.mmp` file you’re currently working on, which is ideal when you’re deep into a proof and want to avoid distractions. 2. **GitHub Copilot Integration** If you’re using **GitHub Copilot** (which is kind of free for GitHub users—likely all of us here), you can enable it in your workspace. It works seamlessly alongside Yamma and provides continuous, non-intrusive suggestions. While the suggestions are not so good yet, they’re improving over time. The more proofs Copilot sees, the better it should become at assisting with Metamath-related tasks. Have fun! Glauco -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/c362312d-93c3-4a49-b27e-e7c6baebd6c1n%40googlegroups.com.
