On Wed, 4 Sep 2013, Holger Gast wrote:
The attached class RetriggeringFlowLayout fixes this problem by caching
the previous size decision from the top-down phase and re-triggering the
layout if that decision has changed.
Thanks, I will look later to see how this is done. Although I don't
believe in anything that "fixes" something, especially not on Java/Swing.
Whatever is done, it will break something else.
Doing some web search myself some months ago, I've found the WrapLayout of
http://tips4java.wordpress.com/2008/11/06/wrap-layout/ but that is already
quite old.
A quite different approach is to make the Find and Sledgehammer panels
more like the regular Find dialog in jEdit, with its way of doing the
layout in a more rigid manner.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
