Skip to content

Commit 7e24f3f

Browse files
authored
Merge pull request #5552 from dotty-staging/fix/worksheet-race-condition
Fix race condition in worksheet output
2 parents f787d11 + 843d595 commit 7e24f3f

File tree

1 file changed

+57
-23
lines changed

1 file changed

+57
-23
lines changed

vscode-dotty/src/worksheet.ts

Lines changed: 57 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,13 @@ export const worksheetRunKey = "dotty.worksheet.run"
2323
*/
2424
export const worksheetCancelKey = "dotty.worksheet.cancel"
2525

26+
/**
27+
* If true, the setting for running the worksheet on save is enabled.
28+
*/
29+
function runWorksheetOnSave(): boolean {
30+
return vscode.workspace.getConfiguration("dotty").get("runWorksheetOnSave") as boolean
31+
}
32+
2633
/**
2734
* A wrapper around the information that VSCode needs to display text decorations.
2835
*
@@ -63,6 +70,14 @@ class Worksheet implements Disposable {
6370
*/
6471
private canceller?: CancellationTokenSource = undefined
6572

73+
/**
74+
* The edits that should be applied to this worksheet.
75+
*
76+
* This is used to ensure that the blank lines added to fit the output of the worksheet
77+
* are inserted in the same order as the output arrived.
78+
*/
79+
private applyEdits: Promise<void> = Promise.resolve()
80+
6681
constructor(readonly document: vscode.TextDocument, readonly client: BaseLanguageClient) {
6782
}
6883

@@ -73,7 +88,7 @@ class Worksheet implements Disposable {
7388
this.canceller = undefined
7489
}
7590
this._onDidStateChange.dispose()
76-
}
91+
}
7792

7893
/** Remove all decorations, and resets this worksheet. */
7994
private reset(): void {
@@ -83,6 +98,7 @@ class Worksheet implements Disposable {
8398
this.decoratedLines.clear()
8499
this.runVersion = -1
85100
this.margin = this.longestLine() + 5
101+
this.applyEdits = Promise.resolve()
86102
}
87103

88104
/**
@@ -111,6 +127,13 @@ class Worksheet implements Disposable {
111127
return this.canceller != undefined
112128
}
113129

130+
/** Display the output in the worksheet's editor. */
131+
handleMessage(output: WorksheetPublishOutputParams, editor: vscode.TextEditor) {
132+
this.applyEdits = this.applyEdits.then(() => {
133+
this.displayAndSaveResult(output.line - 1, output.content, editor)
134+
})
135+
}
136+
114137
/**
115138
* Run the worksheet in `document`, if a previous run is in progress, it is
116139
* cancelled first.
@@ -160,10 +183,10 @@ class Worksheet implements Disposable {
160183
* @param runResult The result itself.
161184
* @param worksheet The worksheet that receives the result.
162185
* @param editor The editor where to display the result.
163-
* @return A `Thenable` that will insert necessary lines to fit the output
186+
* @return A `Promise` that will insert necessary lines to fit the output
164187
* and display the decorations upon completion.
165188
*/
166-
public displayAndSaveResult(lineNumber: number, runResult: string, editor: vscode.TextEditor) {
189+
public async displayAndSaveResult(lineNumber: number, runResult: string, editor: vscode.TextEditor): Promise<void> {
167190
const resultLines = runResult.trim().split(/\r\n|\r|\n/g)
168191

169192
// The line where the next decoration should be put.
@@ -183,21 +206,18 @@ class Worksheet implements Disposable {
183206
this.runVersion += 1
184207
}
185208

186-
return vscode.workspace.applyEdit(addNewLinesEdit).then(_ => {
187-
for (let line of resultLines) {
188-
const decorationPosition = new vscode.Position(actualLine, 0)
189-
const decorationMargin = this.margin - editor.document.lineAt(actualLine).text.length
190-
const decorationType = this.createDecoration(decorationMargin, line)
191-
const decorationOptions = { range: new vscode.Range(decorationPosition, decorationPosition), hoverMessage: line }
192-
const decoration = new Decoration(decorationType, decorationOptions)
193-
194-
this.decoratedLines.add(actualLine)
195-
this.decorations.push(decoration)
196-
197-
editor.setDecorations(decorationType, [decorationOptions])
198-
actualLine += 1
199-
}
200-
})
209+
await vscode.workspace.applyEdit(addNewLinesEdit);
210+
for (let line of resultLines) {
211+
const decorationPosition = new vscode.Position(actualLine, 0);
212+
const decorationMargin = this.margin - editor.document.lineAt(actualLine).text.length;
213+
const decorationType = this.createDecoration(decorationMargin, line);
214+
const decorationOptions = { range: new vscode.Range(decorationPosition, decorationPosition), hoverMessage: line };
215+
const decoration = new Decoration(decorationType, decorationOptions);
216+
this.decoratedLines.add(actualLine);
217+
this.decorations.push(decoration);
218+
editor.setDecorations(decorationType, [decorationOptions]);
219+
actualLine += 1;
220+
}
201221
}
202222

203223
/**
@@ -325,11 +345,25 @@ export class WorksheetProvider implements Disposable {
325345
codeLensProvider,
326346
vscode.languages.registerCodeLensProvider(documentSelector, codeLensProvider),
327347
vscode.workspace.onWillSaveTextDocument(event => {
328-
const runWorksheetOnSave = vscode.workspace.getConfiguration("dotty").get("runWorksheetOnSave")
329-
const worksheet = this.worksheetFor(event.document)
348+
const document = event.document
349+
const worksheet = this.worksheetFor(document)
330350
if (worksheet) {
331351
event.waitUntil(Promise.resolve(worksheet.prepareRun()))
332-
if (runWorksheetOnSave) worksheet.run()
352+
// If the document is not dirty, then `onDidSaveTextDocument` will not
353+
// be called so we need to run the worksheet now.
354+
// On the other hand, if the document _is_ dirty, we should _not_ run
355+
// the worksheet now because the server state will not be synchronized
356+
// with the client state, instead we let `onDidSaveTextDocument`
357+
// handle it.
358+
if (runWorksheetOnSave() && !document.isDirty) {
359+
worksheet.run()
360+
}
361+
}
362+
}),
363+
vscode.workspace.onDidSaveTextDocument(document => {
364+
const worksheet = this.worksheetFor(document)
365+
if (worksheet && runWorksheetOnSave()) {
366+
worksheet.run()
333367
}
334368
}),
335369
vscode.workspace.onDidCloseTextDocument(document => {
@@ -404,7 +438,7 @@ export class WorksheetProvider implements Disposable {
404438
* Handle the result of running part of a worksheet.
405439
* This is called when we receive a `worksheet/publishOutput`.
406440
*
407-
* @param message The result of running part of a worksheet.
441+
* @param output The result of running part of a worksheet.
408442
*/
409443
private handleMessage(output: WorksheetPublishOutputParams) {
410444
const editor = vscode.window.visibleTextEditors.find(e => {
@@ -415,7 +449,7 @@ export class WorksheetProvider implements Disposable {
415449
if (editor) {
416450
const worksheet = this.worksheetFor(editor.document)
417451
if (worksheet) {
418-
worksheet.displayAndSaveResult(output.line - 1, output.content, editor)
452+
worksheet.handleMessage(output, editor)
419453
}
420454
}
421455
}

0 commit comments

Comments
 (0)