diff --git a/src/core/watcher.ts b/src/core/watcher.ts index 6a2a77e09..ca6b10971 100644 --- a/src/core/watcher.ts +++ b/src/core/watcher.ts @@ -145,7 +145,7 @@ class Watcher { this.polling[uriString] = { size, time: firstChangeTime } const pollingInterval = setInterval(() => { - void this.handlePolling(uri, size, firstChangeTime, pollingInterval) + void this.handlePolling(uri, firstChangeTime, pollingInterval) }, vscode.workspace.getConfiguration('latex-workshop').get('latex.watch.pdf.delay') as number) } @@ -164,7 +164,7 @@ class Watcher { * @param {number} firstChangeTime - The timestamp of the first change. * @param {NodeJS.Timeout} interval - The polling interval. */ - private async handlePolling(uri: vscode.Uri, size: number, firstChangeTime: number, interval: NodeJS.Timeout): Promise { + private async handlePolling(uri: vscode.Uri, firstChangeTime: number, interval: NodeJS.Timeout): Promise { const uriString = uri.toString(true) if (!await lw.file.exists(uri)) { clearInterval(interval) @@ -174,12 +174,18 @@ class Watcher { const currentSize = (await lw.external.stat(uri)).size - if (currentSize !== size) { + if (currentSize !== this.polling[uriString].size) { this.polling[uriString].size = currentSize this.polling[uriString].time = Date.now() return } + // Resume vscode may cause accidental "change", do nothing + if (!(uriString in this.polling)) { + clearInterval(interval) + return + } + if (Date.now() - this.polling[uriString].time >= 200) { logger.log(`"change" emitted on ${uriString} after polling for ${Date.now() - firstChangeTime} ms.`) clearInterval(interval)