[isabelle-dev] jEdit: Automatic popup menus on hovers

[Alexander Krauss]

> 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 PM, Makarius wrote:
> I've spent some days pondering various possibilities and reading sources
> of Java/Swing libraries.  Not everything is clear, but there are various
> possibilities of memory leaks and timing problems when popping up a new
> window for each tooltip (in the sense of regular getToolTipText of Swing
> components).

Concerning actual memory leaks, I made the experience that these are 
rather easy to track down on the JVM: Take a heap dump and analyze it 
using a suitable tool such as Eclipse Memory Analyzer 
(http://www.eclipse.org/mat/). The tool has an automated analysis which 
can usually point out the main sources of memory consumption immediately.

Alex