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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
