Skip to content

Commit 7087a6c

Browse files
authored
Merge pull request #5238 from dotty-staging/worksheet-stuff-2
Decouple saving and running the worksheet
2 parents 7e5f0a2 + 6640161 commit 7087a6c

File tree

2 files changed

+46
-43
lines changed

2 files changed

+46
-43
lines changed

vscode-dotty/package.json

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,17 @@
4040
]
4141
}
4242
],
43+
"configuration": {
44+
"type": "object",
45+
"title": "Dotty configuration",
46+
"properties": {
47+
"dotty.runWorksheetOnSave": {
48+
"type": "boolean",
49+
"default": true,
50+
"description": "If true, saving a worksheet will also run it."
51+
}
52+
}
53+
},
4354
"commands": [
4455
{
4556
"command": "dotty.worksheet.run",

vscode-dotty/src/worksheet.ts

Lines changed: 35 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
import * as vscode from 'vscode'
2+
import { TextEdit } from 'vscode'
23

34
import {
4-
asWorksheetRunParams, WorksheetRunRequest, WorksheetRunParams,
5+
asWorksheetRunParams, WorksheetRunRequest, WorksheetRunParams, WorksheetRunResult,
56
WorksheetPublishOutputParams, WorksheetPublishOutputNotification
67
} from './protocol'
78
import { BaseLanguageClient, DocumentSelector } from 'vscode-languageclient'
@@ -41,23 +42,35 @@ class Worksheet {
4142

4243
/**
4344
* Reset the "worksheet state" (margin and number of inserted lines), and
44-
* removes redundant blank lines that have been inserted by a previous
45-
* run.
45+
* return an array of TextEdit that remove the redundant blank lines that have
46+
* been inserted by a previous run.
4647
*/
47-
prepareForRunning(): void {
48-
this.removeRedundantBlankLines().then(_ => this.reset())
48+
prepareRun(): TextEdit[] {
49+
const edits = this.removeRedundantBlankLinesEdits()
50+
this.reset()
51+
return edits
4952
}
5053

5154
/**
5255
* Run the worksheet in `document`, display a progress bar during the run.
5356
*/
54-
run(): Thenable<{}> {
55-
return vscode.window.withProgress({
56-
location: vscode.ProgressLocation.Notification,
57-
title: "Run the worksheet",
58-
cancellable: true
59-
}, (_, token) => {
60-
return this.client.sendRequest(WorksheetRunRequest.type, asWorksheetRunParams(this.document), token)
57+
run(): Promise<WorksheetRunResult> {
58+
return new Promise((resolve, reject) => {
59+
const textEdits = this.prepareRun()
60+
const edit = new vscode.WorkspaceEdit()
61+
edit.set(this.document.uri, textEdits)
62+
vscode.workspace.applyEdit(edit).then(editSucceeded => {
63+
if (editSucceeded) {
64+
return resolve(vscode.window.withProgress({
65+
location: vscode.ProgressLocation.Notification,
66+
title: "Run the worksheet",
67+
cancellable: true
68+
}, (_, token) => this.client.sendRequest(
69+
WorksheetRunRequest.type, asWorksheetRunParams(this.document), token
70+
)))
71+
} else
72+
reject()
73+
})
6174
})
6275
}
6376

@@ -143,16 +156,16 @@ class Worksheet {
143156
}
144157

145158
/**
146-
* Remove the repeated blank lines in the source.
159+
* TextEdits to remove the repeated blank lines in the source.
147160
*
148161
* Running a worksheet can insert new lines in the worksheet so that the
149162
* output of a line fits below the line. Before a run, we remove blank
150163
* lines in the worksheet to keep its length under control.
151164
*
152165
* @param worksheet The worksheet where blank lines must be removed.
153-
* @return A `Thenable` removing the blank lines upon completion.
166+
* @return An array of `TextEdit` that remove the blank lines.
154167
*/
155-
private removeRedundantBlankLines() {
168+
private removeRedundantBlankLinesEdits(): TextEdit[] {
156169

157170
const document = this.document
158171
const lineCount = document.lineCount
@@ -188,13 +201,7 @@ class Worksheet {
188201
addRange()
189202
}
190203

191-
return rangesToRemove.reverse().reduce((chain: Thenable<boolean>, range) => {
192-
return chain.then(_ => {
193-
const edit = new vscode.WorkspaceEdit()
194-
edit.delete(document.uri, range)
195-
return vscode.workspace.applyEdit(edit)
196-
})
197-
}, Promise.resolve(true))
204+
return rangesToRemove.reverse().map(range => vscode.TextEdit.delete(range))
198205
}
199206

200207
private hasDecoration(line: number): boolean {
@@ -213,14 +220,14 @@ export class WorksheetProvider implements Disposable {
213220
vscode.workspace.onWillSaveTextDocument(event => {
214221
const worksheet = this.worksheetFor(event.document)
215222
if (worksheet) {
216-
// Block file saving until the worksheet is ready to be run.
217-
worksheet.prepareForRunning()
223+
event.waitUntil(Promise.resolve(worksheet.prepareRun()))
218224
}
219225
}),
220226
vscode.workspace.onDidSaveTextDocument(document => {
227+
const runWorksheetOnSave = vscode.workspace.getConfiguration("dotty").get("runWorksheetOnSave")
221228
const worksheet = this.worksheetFor(document)
222-
if (worksheet) {
223-
return worksheet.run()
229+
if (runWorksheetOnSave && worksheet) {
230+
worksheet.run()
224231
}
225232
}),
226233
vscode.workspace.onDidCloseTextDocument(document => {
@@ -264,28 +271,13 @@ export class WorksheetProvider implements Disposable {
264271

265272
/**
266273
* The VSCode command executed when the user select `Run worksheet`.
267-
*
268-
* We check whether the buffer is dirty, and if it is, we save it. Running the worksheet will then be
269-
* triggered by file save.
270-
* If the buffer is clean, we do the necessary preparation for worksheet (compute margin,
271-
* remove blank lines, etc.) and check if the buffer has been changed by that. If it is, we save
272-
* and the run will be triggered by file save.
273-
* If the buffer is still clean, call `Worksheet#run`.
274274
*/
275275
private runWorksheetCommand() {
276276
const editor = vscode.window.activeTextEditor
277277
if (editor) {
278-
const document = editor.document
279-
const worksheet = this.worksheetFor(document)
278+
const worksheet = this.worksheetFor(editor.document)
280279
if (worksheet) {
281-
if (document.isDirty) document.save() // This will trigger running the worksheet
282-
else {
283-
worksheet.prepareForRunning()
284-
if (document.isDirty) document.save() // This will trigger running the worksheet
285-
else {
286-
worksheet.run()
287-
}
288-
}
280+
worksheet.run()
289281
}
290282
}
291283
}

0 commit comments

Comments
 (0)