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

[Makarius]

On 20/08/2022 16:20, Florian Haftmann wrote:
> 
> in rev. d7e0b6620c07 opening the query panel by clicking on its button
> fails with:
> 
>> java.lang.NullPointerException: Cannot invoke "scala.collection.immutable.List.foreach(scala.Function1)" because "this.isabelle$jedit$Query_Dockable$$operations" is null
>> 	at isabelle.jedit.Query_Dockable.handle_resize$$anonfun$1(query_dockable.scala:303)
>> 	at isabelle.jedit.Query_Dockable.handle_resize$$anonfun$adapted$1(query_dockable.scala:303)
>> 	at isabelle.GUI_Thread$.require(gui_thread.scala:23)
>> 	at isabelle.jedit.Query_Dockable.isabelle$jedit$Query_Dockable$$handle_resize(query_dockable.scala:303)

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