What's Changed

Added

The library we built to pretty print terms has been considerably improved. Drawing from Oppen's algorithm we are now much faster at displaying goals

feat: optimize pp-display for a better and faster goal view and query panel by @rtetley in #900

This lays for the groundwork for further optimisations.

Two new options have been introduced thanks to @Durbatuluk1701:

vscoq.proof.display-buttons provides a way to disable the proof navigation and general buttons from the buffer

feat: add config option to control whether Coq buttons are displayed by @Durbatuluk1701 in #904
vscoq.proof.pointInterpretationMode determines the behaviour of the interpret to mode command, does it consider the sentence under the cursor or not ?
"vscoq.proof.pointInterpretationMode" === Cursor

"vscoq.proof.pointInterpretationMode" === NextCommand

feat: adding option for interpreting to exact cursor position or next command during interpret to point by @Durbatuluk1701 in #875

The query actions now open a prompt window, if the cursor is pointing at a word, it pre-fills the prompt with the given word.

Finally this release introduces the ability to view unfocused goals.

A number of fixes were introduced for hovers. We now differentiate between modules and their components. We also can over hover words containing '

fix: hover for period qualifiers and single quotes in names by @Durbatuluk1701 in #899
fix: off by one error in Hover by @Durbatuluk1701 in #903

Finally, the VsCoq activity bar now only appears when there are coq files present in the workspace

fix: make VsCoq activity bar logo appear only when Coq files present by @Durbatuluk1701 in #897

Note that the previously introduced improvements to pretty printing also solved a number of printing bugs such as printing inductive types.

No new contributors for this release.

Full Changelog: v2.2.0...v2.2.1