Tips

Jump to bottom Edit New page

CJ Bell edited this page Dec 21, 2016 · 4 revisions

Tips

Use the prettify-symbols-mode extension to support fancy notation.
Or see Latex Snippets for a convenient way to insert Unicode characters.
To hide *.{vo, v.d, glob, aux} files from vscode's sidebar, open your user or workspace settings and add:

"files.exclude": {
    "**/*.{vo,v.d,glob,aux,bak}": true
}

Ubuntu + vnc/rdp & can't run vscode? See: https://github.com/Microsoft/vscode/issues/3451
You can manually specify how to load a proof-view externally. For example:
- Mac OS X: "coq.externalViewUrlCommand": "'/Applications/Google Chrome.app/Contents/MacOS/Google Chrome' ${url}"
- "coq.externalViewUrlCommand": "firefox ${url}"