On Tue, 6 Oct 2015, Dmitriy Traytel wrote:
I’m not sure if this is rather something for the jEdit mailing list, but
I try here first. The attached theory is an empty 500+ lines long file
where everything is normal. However, if I add one new line the scrollbar
disappears.
This is a problem of the Nimbus look-and-feel in jdk-8u60 (the current
official release). See also
https://bugs.openjdk.java.net/browse/JDK-8134827
Lets wait and see for the next jdk-8 release. If Oracle does not manage
before our winter release, I might just switch the default to Metal.
That old-fashioned look-and-feel works better with GUI scaling, which is
essential on 4K displays.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
