I just had the situation were I opened a thy file and it simply stayed
pink. Even after I closed all other buffers. Exiting and restarting
jedit helped, but maybe there is some other way?
A suggestion concerning colour: numbers in magenta are on the loude side
and give them more prominence than desirable. If you have a few numbers
in your formula, they completely dominate. I suggest to use the same
colour as for constants.
Tobias
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
