NEWS: more static type-checking in Isabelle/Scala

[Makarius]

*** System ***

* Isabelle/Scala now uses more static type-checking by default, notably
Explicit Nulls (as explained in
https://docs.scala-lang.org/scala3/reference/experimental/explicit-nulls.html).
Notable INCOMPATIBILITY: need to be careful about type T vs. T | Null.
The following operations may help to get rid of the Null part:

   proper_value: A | Null => Option[A]
   _.nn: A | Null => A

The "nn" (non-null) operation is written postfix, like regular method
application. This partial operation will throw NullPointerException on
null. Excessive use of "nn" may indicate a Java-centric programming
style: it is better to use null-free operations from the libraries of
Scala and Isabelle/Scala. As last resort, it also possible to opt-out
from Explicit Nulls for Scala modules as follows:

   import scala.language.unsafeNulls

Note: This extension of Scala3 is not yet a "safe" type-system. Even
with type-checking of Explicit Nulls enabled, the Java/VM can produce
null values by other means, e.g. during object initialization.


This refers to Isabelle/c11edc105209 where "scalac -Yexplicit-nulls" is 
enabled by default, except for HOL codgen output.

I have struggled with our Scala sources for several days, but today everything 
worked on the spot: Isabelle + AFP. (Maybe I have overlooked something.)


	Makarius