Bryan Gin-ge Chen

This seems to have been addressed in VScode: https://github.com/Microsoft/vscode/commit/ea09391fd86584614d2763214e46034e79f63588

Thanks for the info! I think all `vscode-resource` URIs were recently removed in https://github.com/leanprover/vscode-lean/commit/3b60fae4d95079beae2701a1f9a12995367dcece.

Yes, this would indeed be nice. This would best be done in VS Code itself. See these two issues: https://github.com/microsoft/vscode/issues/46471 and https://github.com/microsoft/vscode/issues/2809. However, we did implement a workaround for something...

Thanks for the pointer. It looks like the meat of the code is here: https://github.com/microsoft/vscode-python/blob/bd942a0dadaed64061f0e4b6bb3d7bac6df5b2d2/src/client/common/variables/systemVariables.ts We could probably just copy this into vscode-lean; I'll look into it in a few...

You may have already figured this out, but this is happening because when you change the `publisher`, you're effectively creating a separate extension, since VS Code extensions are identified by...

Sadly, I don't think there's a way to do this with the same `Ctrl-p` `#` keybind, since that pulls up VS Code's symbol search menu and as far as I...

This has also bitten me. I'd support your suggestion to improve TPiL; its repo can be found [here](https://github.com/leanprover/theorem_proving_in_lean/). You might also find Ed Ayers's (draft?) doc on unicode in lean...

This behavior is due to [these lines in `style.css`](https://github.com/leanprover-community/doc-gen/blob/master/style.css#L221-L226). (I've actually never noticed it since I'm using macOS and I changed its annoying default setting to only show scrollbars on...

One thing which is very far from obvious at the moment is that clicking the search button does something totally unrelated to the choices in the drop down menu --...

It might not work for PRs opened from external forks? See e.g. https://github.com/leanprover-community/doc-gen/pull/115#issuecomment-779953415