Merge remote-tracking branch 'vscode-lean/master'

leanprover · May 10, 2021 · ee7f592 · ee7f592
2 parents faa196b + 29a03a8
commit ee7f592
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 7 deletions.
diff --git a/old/src/server.ts b/old/src/server.ts
@@ -96,7 +96,7 @@ export class Server extends leanclient.Server {
             switch (e.error) {
                 case 'stderr':
                     stderrOutput.append(e.chunk);
-                    stderrOutput.show();
+                    stderrOutput.show(true);
                     break;
                 case 'connect':
                     // json parsing errors
@@ -180,7 +180,7 @@ export class Server extends leanclient.Server {
             // Now show the terminal and run elan.
             terminal.show();
             terminal.sendText(
-              'curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh && ' +
+              'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh && ' +
               'echo && read -n 1 -s -r -p "Press any key to start Lean" && exit\n');
         }
     }

diff --git a/src/abbreviation/rewriter/AbbreviationRewriter.ts b/src/abbreviation/rewriter/AbbreviationRewriter.ts
@@ -156,8 +156,9 @@ export class AbbreviationRewriter {
 
 		// We don't want replaced symbols (e.g. "\") to trigger abbreviations.
 		this.dontTrackNewAbbr = true;
+		let ok = false;
 		try {
-			await this.textEditor.edit((builder) => {
+			ok = await this.textEditor.edit((builder) => {
 				for (const r of replacements) {
 					builder.replace(
 						toVsCodeRange(r.range, this.textEditor.document),
@@ -170,10 +171,17 @@ export class AbbreviationRewriter {
 		}
 		this.dontTrackNewAbbr = false;
 
-		this.textEditor.selections = newSelections.map((s) => {
-			const vr = toVsCodeRange(s, this.textEditor.document);
-			return new vscode.Selection(vr.start, vr.end);
-		});
+		if (ok) {
+			this.textEditor.selections = newSelections.map((s) => {
+				const vr = toVsCodeRange(s, this.textEditor.document);
+				return new vscode.Selection(vr.start, vr.end);
+			});
+		}
+		else {
+			// Our edit did not succeed, do not update the selections.
+			// This can happen if `waitForNextTick` waits too long.
+			console.warn('Unable to replace abbreviation');
+		}
 
 		this.updateState();
 	}