Hi,
Sometimes jedit does not render math symbols for me, but show their plain ascii source like this:
Screenshot-2024-03-15-at-21.27.10.png
How do I make sure it always renders math symbols for all documents?
I have the same issue on both Isabelle2021 and 2023.
Thanks a lot,
Chengsong
https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Github/near/204994308
Last updated: Dec 30 2024 at 16:22 UTC