API Request: onDidChangeTextDocument - differentiate between user input and redo/undo #120617
Labels
api
api-proposal
editor-core
Editor basic functionality
feature-request
Request for new features or functionality
verification-needed
Verification of issue is requested
verified
Verification succeeded
Milestone
The extension API of VS Code 1.54.3 offers the event
workspace.onDidChangeTextDocument
that can be used to subscribe to text changes.Currently, it does not seem to be possible to differentiate between text changes caused by user-input and those caused by redo/undo.
This is problematic if an extension wants to use the
onDidChangeTextDocument
event to modify the document when certain characters are typed by the user.For example, the abbreviation rewrite feature of the Lean VS Code extension makes use of it (if the user types
\alpha
it gets replaced byα
immediately).However, if the user undoes and redoes their changes,
onDidChangeTextDocument
is also triggered. When undoing/redoing, new text edits are very harmful though, as they destroy the redo stack. Thus, extensions must not modify the document on redos/undos.If
redos
cannot be differentiated from user input, this problem cannot be avoided if an extension wants to modify the document on certain text changes.Proposal
It would be helpful if VS Code could provide a reason that caused the text change.
Reasons could be:
userInput
: The user typed a character.redo
: Caused by redoundo
: Caused by undounknown
: E.g. caused by liveshare or use of workspace.applyEditThe reason could be provided by the
TextDocumentChangeEvent
:Thank you!
The text was updated successfully, but these errors were encountered: