--- 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.
--- 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":