Skip to content

Commit 11e15f0

Browse files
switched parameter order of rascal/edit event to fix #1049 (#1059)
* switched parameter order of rascal/edit event to fix #1049 * Update rascal-vscode-extension/src/lsp/RascalLSPConnection.ts Co-authored-by: Rodin Aarssen <rodin.aarssen@swat.engineering> * Update rascal-vscode-extension/src/lsp/RascalLSPConnection.ts Co-authored-by: Rodin Aarssen <rodin.aarssen@swat.engineering> * Update rascal-vscode-extension/src/lsp/RascalLSPConnection.ts Co-authored-by: Rodin Aarssen <rodin.aarssen@swat.engineering> --------- Co-authored-by: Rodin Aarssen <rodin.aarssen@swat.engineering>
1 parent c38acff commit 11e15f0

1 file changed

Lines changed: 7 additions & 5 deletions

File tree

rascal-vscode-extension/src/lsp/RascalLSPConnection.ts

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ export async function activateLanguageClient(
6363
});
6464

6565

66-
client.onNotification("rascal/editDocument", (uri: string, viewColumn: integer, range: vscode.Range) => {
66+
client.onNotification("rascal/editDocument", (uri: string, range: vscode.Range | undefined, viewColumn: integer) => {
6767
openEditor(uri, range, viewColumn);
6868
});
6969

@@ -111,7 +111,7 @@ async function showContentPanel(url: string, title:string, viewColumn:integer):
111111
contentPanels.set(id, panel);
112112
}
113113

114-
async function openEditor(uriString: string, range:vscode.Range, viewColumn: integer) {
114+
async function openEditor(uriString: string, range: vscode.Range | undefined, viewColumn: integer) {
115115
const uri = vscode.Uri.parse(uriString);
116116

117117
const doc = await vscode.workspace.openTextDocument(uri);
@@ -127,9 +127,11 @@ async function openEditor(uriString: string, range:vscode.Range, viewColumn: int
127127
// don't use the `selection` field here because we can not control scrolling behavior from that with editors which are already open
128128
});
129129

130-
// set the primary selection and move it into view (but don't scroll unless necessary)
131-
editor.selection = new vscode.Selection(range.start, range.end);
132-
editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport);
130+
if (range !== undefined) {
131+
// set the primary selection and move it into view (but don't scroll unless necessary)
132+
editor.selection = new vscode.Selection(range.start, range.end);
133+
editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport);
134+
}
133135
}
134136

135137

0 commit comments

Comments
 (0)