Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Query panel not working in rev. d7e0b6620c07

view this post on Zulip Email Gateway (Aug 20 2022 at 14:20):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

in rev. d7e0b6620c07 opening the query panel by clicking on its button
fails with:

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Aug 20 2022 at 21:59):

From: Makarius <makarius@sketis.net>
Thanks for keeping an eye (or two) on it. I have amended that here:

changeset: 75922:4586e90573ac
user: wenzelm
date: Sat Aug 20 21:33:51 2022 +0200
files: src/Tools/jEdit/src/query_dockable.scala
description:
more robust GUI initialization (amending 29441f2bfe81);

changeset: 75839:29441f2bfe81
user: wenzelm
date: Sat Aug 13 12:32:38 2022 +0200
files: src/Pure/GUI/gui.scala src/Tools/Graphview/graph_panel.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/document_dockable.scala
src/Tools/jEdit/src/font_info.scala src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/jedit_spell_checker.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/state_dockable.scala
description:
clarified signature: more explicit types;
more robust zoom.factor: work with uninitialized GUI components;

The changeset 29441f2bfe81 was not fully successful in addressing
"uninitialized GUI components".

Even when using static types and immutable values, Scala can crash with NPEs,
because the order of object initialization matters. Accessing values
out-of-order will not work, as we have seen here.

A common workaround is to sprinkle objects with "lazy val ..." declarations,
but that can lead to non-termination instead.

So we need to stay honest and acknowledge that types in Scala/Java are only an
approximative tool to improve software quality.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Dec 21 2024 at 16:20 UTC