--- a/ANNOUNCE Wed Nov 05 12:34:45 2025 +0100
+++ b/ANNOUNCE Wed Nov 05 12:57:55 2025 +0100
@@ -1,41 +1,43 @@
-Subject: Announcing Isabelle2025
+Subject: Announcing Isabelle2025-1
To: isabelle-users@cl.cam.ac.uk
-Isabelle2025 is now available.
+Isabelle2025-1 is now available.
-This version introduces many changes over Isabelle2024: see the
-NEWS file for further details. Here are various details:
+This version introduces many changes over Isabelle2025: see the
+NEWS file for further details. Here are notable details:
+
+* PIDE: load markup from background session image (e.g. theory "HOL.Nat").
+
+* Isabelle/jEdit: support for command-line system options ("-o").
-* Inner syntax: markup for blocks and type information about constants.
+* Isabelle/jEdit: support for dark mode and screen readers.
-* Inner syntax: more scalable pretty-printing, based on bytes (blobs).
+* Isabelle/jEdit: built-in navigator, without requiring plugins.
+
+* Isabelle/jEdit: updated FlatLaf GUI L&F with scalable SVG icons.
-* Inner syntax: more efficient folding of term abbreviations.
+* Isabelle/jEdit: improved appearance on Linux (GUI scaling) and macOS (L&F).
-* Inner syntax: more robust "no_syntax" declarations via bundles.
+* Isabelle/VSCode: GUI panels for Documentation, Symbols, Sledgehammer.
+
+* Isabelle/VSCode: update of underlying VSCodium distribution.
* HOL: various improvements of theory libraries.
-* HOL: updates and improvements of Sledgehammer and external provers.
-
* HOL: various improvements to code generation.
-* Isabelle/jEdit: various improvements to Output, including Search.
+* HOL: updates and improvements of Sledgehammer and external provers.
-* Isabelle/VSCode: various improvements, concerning markup, completions etc.
-
-* Document preparation: more markup for term output.
+* System: ML settings may depend on command-line system options ("-o").
-* ML: value-oriented pretty printing using explicit Pretty.output_ops.
-
-* System: Find_Facts full-text search engine, with web interface.
+* System: command-line tool to process theories within adhoc session.
-* System: Build_Manager in Isabelle/Scala, as replacement for Jenkins.
+* System: more detailed build progress.
-* System: more scalable type isabelle.Bytes, allow messages of many GiB.
+* System: more robust build cluster management.
-You may get Isabelle2025 from the following mirror sites:
+You may get Isabelle2025-1 from the following mirror sites:
Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle
Munich (Germany) https://isabelle.in.tum.de