Hi Marlo,
I use Yamma (a VSCode extension). A Unicode view would be great — I’ve been thinking about how to implement it, but I haven’t figured out an effective way to display it without taking up too much video space (which is already barely enough to show long wffs). An even cooler idea might be to allow writing .mmp files directly in Unicode, with the PA translating them to ASCII under the hood. This would also make it possible to define "custom" symbols specific to a given .mmp file — for example, you could locally define the Unicode integral symbol to represent one of the many integrals defined in set.mm. -- 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/1c497904-b3bb-4b2f-8be2-a7b254d156d2n%40googlegroups.com.
