# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1727869801 -7200
# Node ID 9c2628a73a3a12ea4652a0268fc2cbe44d06a897
# Parent  fe69241e87867df2965cd055740849e9ac0e25d5
NEWS and CONTRIBUTORS;

diff -r fe69241e8786 -r 9c2628a73a3a CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Oct 02 10:51:11 2024 +0200
+++ b/CONTRIBUTORS	Wed Oct 02 13:50:01 2024 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* April - October 2024: Thomas Lindae and Fabian Huch, TU München
+  Improvements to the language server for Isabelle/VSCode.
+
 * June - July 2024: Fabian Huch
   New Build_Manager module to coordinate CI and user builds, replacing
   the previous Jenkins integration.
diff -r fe69241e8786 -r 9c2628a73a3a NEWS
--- a/NEWS	Wed Oct 02 10:51:11 2024 +0200
+++ b/NEWS	Wed Oct 02 13:50:01 2024 +0200
@@ -26,6 +26,21 @@
 "cong" rules, notably for congproc implementations.
 
 
+*** Isabelle/VSCode Prover IDE ***
+
+* General improvements: Persistent decorations for PIDE markup, correct
+  font and formatting in panels, and proper completions.
+  Moreover, the PIDE extension of the LSP now features additional
+  protocol messages (e.g. to obtain the set of Isabelle symbols) and
+  more fine-grained control for unicode symbols.
+
+* Active "sendback" markup can now be used via LSP code actions, e.g.
+  to insert proof methods from Sledgehammer output.
+
+* Relevant Isabelle options can now be overriden from the
+  Isabelle/VSCode extension settings.
+
+
 *** HOL ***
 
 * Theory "HOL.Wellfounded":