NEWS: Isabelle2025-2 supersedes Isabelle2025-1

[Makarius]

Due to a notable confusion of options for isabelle build, the release of 
Isabelle2025-1 (December 2025) had to be replaced on the spot by 
Isabelle2025-2 (January 2026).

The relevant NEWS entries are as follows:


*** General ***

* Command 'sorry' is rejected by "isabelle build" as expected, with the
default option "quick_and_dirty=false". This was broken in
Isabelle2025-1: Isar commands were considered interactive due to the
default option "show_results=true". Proper behaviour could be recovered
in Isabelle2025-1 via "isabelle build -o show_results=false", but it is
better to use Isabelle2025-2. Both approaches result in minor changes of
result messages stored in session build databases.


*** Isabelle/jEdit Prover IDE ***

* Console/Scala: proper treatment of interrupts via "Stop" button. It
was broken since Isabelle2022: Scala interpreter thread became
inoperative afterwards.


This refers to Isabelle/89701cf1768e.


The release website requires some time to be fully updated, including all 
mirrors. Afterwards, I will make a proper announcement on isabelle-users.

The plan for Isabelle2026 (October 2026) remains unchanged: 
https://sketis.net/2025/plan-for-isabelle2026-october-2026 --- thus we have 
sufficient distance to the Christmas vacation.


The last time we've had the awkward situation to have one release supersede 
another was Isabelle2013-2: 
https://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/NEWS --- 
there were many more posthoc changes, and I was really worried about the 
overall state of affairs.

We have recovered from that pretty well in 2014/2015 by removing old system 
variations that no longer had a purpose (TTY REPL and Proof General Emacs), 
and by relying more on Isabelle/Scala than the somewhat accidental 
operating-system environment.

Abstractly, the same idea is still relevant: this time it will be the removal 
of the remains of ML-toplevel build (use_thy), together with odd historic 
options like "interactive mode" for Isar commands. Regular system options are 
sufficient (module Options in Isabelle/ML and Isabelle/Scala).


	Makarius