On Sat, 9 Mar 2013, Lars Noschinski wrote:
I'm currently using revision 4b5a5e26161d of Isabelle and after working
with it for one day without stopping jEdit, I noticed a annoying
behaviour of the popup menus which you get automatically by hovering
over a command with a message:
They pop up
On Sat, 9 Mar 2013, Lars Noschinski wrote:
This behaviour only popped up after working with one session for a
longer time and jEdit was having frequent hiccups then, so I guess
this was due to memory pressure (max memory usage was near the limit
of 1600m set for the JVM).
On 03/18/2013 01:29
Hi,
I'm currently using revision 4b5a5e26161d of Isabelle and after working
with it for one day without stopping jEdit, I noticed a annoying
behaviour of the popup menus which you get automatically by hovering
over a command with a message:
They pop up immediately, even if I don't stop over
