[isabelle-dev] jedit

[Tobias Nipkow]

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