development/vscode
development/vscode
1
0
Fork 0
mirror of https://github.com/Microsoft/vscode synced 2024-08-27 04:49:35 +00:00
Code Issues Packages Projects Releases Wiki Activity

[Bug] /var/folders/** files can't be excluded from search (fix #203872) (#208296)

Browse source
This commit is contained in:
Benjamin Pasero 2024-03-21 13:01:42 +01:00 committed by GitHub
parent b1229cc440
commit 8a19756adf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 39 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
src/vs/workbench/services/history/browser/historyService.ts
View file

@ -819,35 +819,43 @@ export class HistoryService extends Disposable implements IHistoryService {
this.editorHelper.clearOnEditorDispose(this.history.pop()!, this.editorHistoryListeners);
}
// React to editor input disposing if this is a typed editor
if (isEditorInput(historyInput)) {
this.editorHelper.onEditorDispose(historyInput, () => this.updateHistoryOnEditorDispose(historyInput), this.editorHistoryListeners);
// React to editor input disposing
if (isEditorInput(editor)) {
this.editorHelper.onEditorDispose(editor, () => this.updateHistoryOnEditorDispose(historyInput), this.editorHistoryListeners);
}
}
private updateHistoryOnEditorDispose(editor: EditorInput): void {
private updateHistoryOnEditorDispose(editor: EditorInput | IResourceEditorInput): void {
if (isEditorInput(editor)) {
// Any non side-by-side editor input gets removed directly on dispose
if (!isSideBySideEditorInput(editor)) {
this.removeFromHistory(editor);
}
// Side-by-side editors get special treatment: we try to distill the
// possibly untyped resource inputs from both sides to be able to
// offer these entries from the history to the user still.
else {
const resourceInputs: IResourceEditorInput[] = [];
const sideInputs = editor.primary.matches(editor.secondary) ? [editor.primary] : [editor.primary, editor.secondary];
for (const sideInput of sideInputs) {
const candidateResourceInput = this.editorHelper.preferResourceEditorInput(sideInput);
if (isResourceEditorInput(candidateResourceInput)) {
resourceInputs.push(candidateResourceInput);
}
// Any non side-by-side editor input gets removed directly on dispose
if (!isSideBySideEditorInput(editor)) {
this.removeFromHistory(editor);
}
// Insert the untyped resource inputs where our disposed
// side-by-side editor input is in the history stack
this.replaceInHistory(editor, ...resourceInputs);
// Side-by-side editors get special treatment: we try to distill the
// possibly untyped resource inputs from both sides to be able to
// offer these entries from the history to the user still.
else {
const resourceInputs: IResourceEditorInput[] = [];
const sideInputs = editor.primary.matches(editor.secondary) ? [editor.primary] : [editor.primary, editor.secondary];
for (const sideInput of sideInputs) {
const candidateResourceInput = this.editorHelper.preferResourceEditorInput(sideInput);
if (isResourceEditorInput(candidateResourceInput)) {
resourceInputs.push(candidateResourceInput);
}
}
// Insert the untyped resource inputs where our disposed
// side-by-side editor input is in the history stack
this.replaceInHistory(editor, ...resourceInputs);
}
} else {
// Remove any editor that should not be included in history
if (!this.includeInHistory(editor)) {
this.removeFromHistory(editor);
}
}
}
@ -1019,7 +1027,10 @@ export class HistoryService extends Disposable implements IHistoryService {
// We check on resource and `editorId` (from `override`)
// to figure out if the editor has been already added.
for (const editor of storedEditorHistory) {
if (!handledEditors.has(`${editor.resource.toString()}/${editor.options?.override}`)) {
if (
!handledEditors.has(`${editor.resource.toString()}/${editor.options?.override}`) &&
this.includeInHistory(editor)
) {
this.addToHistory(editor, false /* at the end */);
}
}
@ -1162,6 +1173,10 @@ export class HistoryService extends Disposable implements IHistoryService {
stack.disposable.dispose();
}
}
for (const [, listener] of this.editorHistoryListeners) {
listener.dispose();
}
}
}