# HG changeset patch # User Fabian Huch # 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":