On 03/07/17 21:14, Simon Wimmer wrote: > > One thing that disturbed me in the beginning was that I first have to > edit a document before any symbols get prettified.
This might be a weakness of the Prettify Symbols Mode, or just a mistake in setting it up on my side. (For months, I have not heard anything from its author CJ Bell, who is also the guy behind VSCoq.) In the section about limitations in src/Tools/VSCode/extension/README.md, I wrote: * Isabelle symbols are merely an optical illusion: it would be better to make them a first-class Unicode charset as in Isabelle/jEdit. This would also solve the Unicode copy-paste confusion, and make it work as in Isabelle/jEdit. Doing that might require a small patch here https://github.com/Microsoft/vscode/blob/master/src/vs/base/node/encoding.ts and then to rebuild/rebrand/repackage the whole VSCode/Electron application. I still need to figure out how this works in the first place ... Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev