Email Gateway (Aug 23 2022 at 08:40): Email Gateway (Aug 23 2022 at 08:40):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Running Isabelle2020-RC2 under Ubuntu 18.04, I opened the "Global Options" window and under "jedit/Text Area",
I cleared the input box under "Extra vertical line spacing (in pixels)", which previously contained "1".
Clicking "Apply" triggered a "NumberFormatException" stack trace (see below). Putting "0" in the box and
clicking "Apply" did not trigger the spew. Probably an empty string is not valid as input to this box,
but it should fail gracefully and inform the user properly.
Email Gateway (Aug 23 2022 at 08:41):From: Makarius <makarius@sketis.net>
I can confirm this, even with Java 8 and jEdit 5.4.0 --- while
Isabelle2020-RC2 is using Java 11 and jEdit 5.5.0.
The problem is one of jEdit, not Isabelle/jEdit. You can submit tickets here:
https://sourceforge.net/p/jedit/bugs
There is presently a little bit of development activity on the jEdit project,
so contributions by careful users will provide further motivation to sort it
all out.
Makarius
Email Gateway (Aug 23 2022 at 08:41):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
OK.
I think the real mistake was the Java libraries making NumberFormatException a subclass of RuntimeException.
Last updated: Nov 21 2024 at 12:39 UTC