The document that the edit is for.
Display name describing the edit.
This will be shown to users in the UI for undo/redo operations.
Redo the edit operation.
This is invoked by Theia when the user redoes this edit. To implement redo
, your
extension should restore the document and editor to the state they were in just after this
edit was added to Theia's internal edit stack by onDidChangeCustomDocument
.
Undo the edit operation.
This is invoked by Theia when the user undoes this edit. To implement undo
, your
extension should restore the document and editor to the state they were in just before this
edit was added to Theia's internal edit stack by onDidChangeCustomDocument
.
Event triggered by extensions to signal that an edit has occurred on an
CustomDocument
.CustomEditorProvider.onDidChangeCustomDocument.