diff --git a/README.md b/README.md
index 4a99fb7..9232ff6 100644
--- a/README.md
+++ b/README.md
@@ -62,6 +62,7 @@ It also contributes the following commands, which can be bound to keys if desire
* `lean.infoView.displayGoal`: show the tactic state and any messages (e.g. info, warning, error) at the current position in the info view window (bound to ctrl+shift+enter by default)
* `lean.infoView.displayList`: show all messages for the current file from Lean in the info view window (bound to ctrl+shift+alt+enter by default)
* `lean.infoView.copyToComment`: copy the current contents of the info view into a new comment on the next line
+* `lean.infoView.toggleStickyPosition`: enable / disable "sticky" mode. On enable this places a marker at the current position, and the goal will continue to be reported from this position even as the cursor moves and edits are made to the file. Disabling the mode goes back to tracking the cursor.
* `lean.infoView.toggleUpdating`: pause / continue live updates of the info view (same as clicking on the 
and 
icons)
* `lean.roiMode.select`: select the region of interest (files to be checked by the Lean server)
* `lean.batchExecute`: execute the current file using Lean (bound to ctrl+shift+r by default)
diff --git a/package-lock.json b/package-lock.json
index 511d436..bd1a331 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -327,7 +327,7 @@
"argparse": {
"version": "1.0.10",
"resolved": "https://registry.npmjs.org/argparse/-/argparse-1.0.10.tgz",
- "integrity": "sha512-o5Roy6tNG4SL/FOkCAN6RzjiakZS25RLYFrcMttJqbdd8BWrnA+fGz57iN5Pb06pvBGvl5gQ0B48dJlslXvoTg==",
+ "integrity": "sha1-vNZ5HqWuCXJeF+WtmIE0zUCz2RE=",
"dev": true,
"requires": {
"sprintf-js": "~1.0.2"
@@ -410,7 +410,7 @@
"brace-expansion": {
"version": "1.1.11",
"resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz",
- "integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==",
+ "integrity": "sha1-PH/L9SnYcibz0vUrlm/1Jx60Qd0=",
"dev": true,
"requires": {
"balanced-match": "^1.0.0",
@@ -572,7 +572,7 @@
"debug": {
"version": "3.1.0",
"resolved": "https://registry.npmjs.org/debug/-/debug-3.1.0.tgz",
- "integrity": "sha512-OX8XqP7/1a9cqkxYw2yXss15f26NKWBpDXQd0/uK/KPqdQhxbPa994hnzjcE2VqQpDslf55723cKPUOGSmMY3g==",
+ "integrity": "sha1-W7WgZyYotkFJVmuhaBnmFRjGcmE=",
"requires": {
"ms": "2.0.0"
}
@@ -625,7 +625,7 @@
"domhandler": {
"version": "2.4.2",
"resolved": "https://registry.npmjs.org/domhandler/-/domhandler-2.4.2.tgz",
- "integrity": "sha512-JiK04h0Ht5u/80fdLMCEmV4zkNh2BcoMFBmZ/91WtYZ8qVXSKjiw7fXMgFPnHcSZgOo3XdinHvmnDUeMf5R4wA==",
+ "integrity": "sha1-iAUJfpM9ZehVRvcm1g9euItE+AM=",
"requires": {
"domelementtype": "1"
}
@@ -793,7 +793,7 @@
"esprima": {
"version": "4.0.1",
"resolved": "https://registry.npmjs.org/esprima/-/esprima-4.0.1.tgz",
- "integrity": "sha512-eGuFFw7Upda+g4p+QHvnW0RyTX/SVeJBDM/gCtMARO0cLuT2HcEKnTPvhjV6aGeqrCB/sbNop0Kszm0jsaWU4A==",
+ "integrity": "sha1-E7BM2z5sXRnfkatph6hpVhmwqnE=",
"dev": true
},
"esquery": {
@@ -1294,7 +1294,7 @@
"json-parse-better-errors": {
"version": "1.0.2",
"resolved": "https://registry.npmjs.org/json-parse-better-errors/-/json-parse-better-errors-1.0.2.tgz",
- "integrity": "sha512-mrqyZKfX5EhL7hvqcV6WG1yYjnjeuYDzDhhcAAUrq8Po85NBQBJP+ZDUT75qZQ98IkUoBqdkExkukOU7Ts2wrw=="
+ "integrity": "sha1-u4Z8+zRQ5pEHwTHRxRS6s9yLyqk="
},
"json-schema-traverse": {
"version": "0.4.1",
@@ -1311,7 +1311,7 @@
"lean-client-js-core": {
"version": "1.2.12",
"resolved": "https://registry.npmjs.org/lean-client-js-core/-/lean-client-js-core-1.2.12.tgz",
- "integrity": "sha512-m2TWFAbokO/ar2hhZupOLMpGf/dAtghRSCbR9xyaYRo37UfztjZ7AAXGm9BF99o/0WZ3Bl2na8ZkYk63H/qnNw==",
+ "integrity": "sha1-nXWRm6H0CwzHnUJ0aNe+eevpS2I=",
"requires": {
"@types/node": "^9.4.6"
},
@@ -1326,7 +1326,7 @@
"lean-client-js-node": {
"version": "1.2.12",
"resolved": "https://registry.npmjs.org/lean-client-js-node/-/lean-client-js-node-1.2.12.tgz",
- "integrity": "sha512-hjsfa0cCQ5ZW3OwvWmbFcgdVmNfIXUfG2r/bXnCyS0yTOlnhFjor6xTud6gNUAQp5FxGMZd0WpwxOMmbYiVaHg==",
+ "integrity": "sha1-DolksMCZUmJJ8OjBY/y1w9uV3FU=",
"requires": {
"@types/node": "^9.4.6",
"lean-client-js-core": "^1.2.12"
@@ -1448,7 +1448,7 @@
"mime": {
"version": "1.6.0",
"resolved": "https://registry.npmjs.org/mime/-/mime-1.6.0.tgz",
- "integrity": "sha512-x0Vn8spI+wuJ1O6S7gnbaQg8Pxh4NNHb7KSINmEWKiPE4RKOplvijn+NkmYmmRgP68mc70j2EbeTFRsrswaQeg=="
+ "integrity": "sha1-Ms2eXGRVO9WNGaVor0Uqz/BJgbE="
},
"mime-db": {
"version": "1.44.0",
@@ -1471,7 +1471,7 @@
"minimatch": {
"version": "3.0.4",
"resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.0.4.tgz",
- "integrity": "sha512-yJHVQEhyqPLUTgt9B83PXu6W3rx4MvvHvSUvToogpwoGDOUQ+yDrR0HRot+yOCdCO7u4hX3pWft6kWBBcqh0UA==",
+ "integrity": "sha1-UWbihkV/AzBgZL5Ul+jbsMPTIIM=",
"dev": true,
"requires": {
"brace-expansion": "^1.1.7"
@@ -1595,7 +1595,7 @@
"osenv": {
"version": "0.1.5",
"resolved": "https://registry.npmjs.org/osenv/-/osenv-0.1.5.tgz",
- "integrity": "sha512-0CWcCECdMVc2Rw3U5w9ZjqX6ga6ubk1xDVKxtBQPK7wis/0F2r9T6k4ydGYhecl7YUBxBVxhL5oisPsNxAPe2g==",
+ "integrity": "sha1-hc36+uso6Gd/QW4odZK18/SepBA=",
"dev": true,
"requires": {
"os-homedir": "^1.0.0",
@@ -1649,7 +1649,7 @@
"parse5": {
"version": "3.0.3",
"resolved": "https://registry.npmjs.org/parse5/-/parse5-3.0.3.tgz",
- "integrity": "sha512-rgO9Zg5LLLkfJF9E6CCmXlSE4UVceloys8JrFqCcHloC3usd/kJCyPDwH2SOlzix2j3xaP9sUX3e8+kvkuleAA==",
+ "integrity": "sha1-BC95L/3TaFFVHPTp4Gazh0q0W1w=",
"requires": {
"@types/node": "*"
}
@@ -1806,7 +1806,7 @@
"safe-buffer": {
"version": "5.1.2",
"resolved": "https://registry.npmjs.org/safe-buffer/-/safe-buffer-5.1.2.tgz",
- "integrity": "sha512-Gd2UZBJDkXlY7GbJxfsE8/nvKkUEU1G38c1siN6QP6a9PT9MmHB8GnpscSmMJSoF8LOIrt8ud/wPtojys4G6+g=="
+ "integrity": "sha1-mR7GnSluAxN0fVm9/St0XDX4go0="
},
"safer-buffer": {
"version": "2.1.2",
diff --git a/package.json b/package.json
index 506f1eb..c938c82 100644
--- a/package.json
+++ b/package.json
@@ -240,6 +240,12 @@
"title": "Info View: Copy Contents to Comment",
"description": "Copy the current contents of the info view into a new comment on the next line."
},
+ {
+ "command": "lean.infoView.toggleStickyPosition",
+ "category": "Lean",
+ "title": "Info View: Toggle Sticky Position",
+ "description": "Mark the current position of the cursor for goal reporting, instead of tracking the cursor."
+ },
{
"command": "lean.infoView.toggleUpdating",
"category": "Lean",
@@ -376,6 +382,10 @@
"command": "lean.infoView.copyToComment",
"when": "editorLangId == lean"
},
+ {
+ "command": "lean.infoView.toggleStickyPosition",
+ "when": "editorLangId == lean"
+ },
{
"command": "lean.infoView.displayGoal",
"when": "resourceSchema == lean-info"
diff --git a/src/infoview.ts b/src/infoview.ts
index 5b16f03..e08cb7f 100644
--- a/src/infoview.ts
+++ b/src/infoview.ts
@@ -43,6 +43,7 @@ export class InfoProvider implements Disposable {
private started: boolean = false;
private stopped: boolean = false;
+ private stickyPosition: boolean = false;
private curFileName: string = null;
private curPosition: Position = null;
private curGoalState: string = null;
@@ -53,6 +54,7 @@ export class InfoProvider implements Disposable {
private messageFormatters: ((text: string, msg: Message) => string)[] = [];
private hoverDecorationType: TextEditorDecorationType;
+ private stickyDecorationType: TextEditorDecorationType;
constructor(private server: Server, private leanDocs: DocumentSelector, private context: ExtensionContext, private staticServer: StaticServer) {
@@ -62,6 +64,10 @@ export class InfoProvider implements Disposable {
backgroundColor: 'red', // make configurable?
border: '3px solid red',
});
+ this.stickyDecorationType = window.createTextEditorDecorationType({
+ backgroundColor: 'blue', // make configurable?
+ border: '3px solid blue',
+ });
this.updateStylesheet();
this.subscriptions.push(
this.server.allMessages.on(() => {
@@ -86,6 +92,35 @@ export class InfoProvider implements Disposable {
this.statusShown = false;
}
}),
+ workspace.onDidChangeTextDocument((e) => {
+ if (this.stickyPosition && this.curPosition != null &&
+ e.document.fileName === this.curFileName) {
+ // stupid cursor math that should be in the vscode API
+ let newPosition = this.curPosition;
+ for (const chg of e.contentChanges) {
+ if (newPosition.isAfterOrEqual(chg.range.start)) {
+ let lines = 0;
+ for (const c of chg.text) if (c === '\n') lines++;
+ newPosition = new Position(
+ chg.range.start.line + Math.max(0, newPosition.line - chg.range.end.line) + lines,
+ newPosition.line > chg.range.end.line ?
+ newPosition.character :
+ lines === 0 ?
+ chg.range.start.character + Math.max(0, newPosition.character - chg.range.end.character) + chg.text.length :
+ 9999 // too lazy to get column positioning right, and end of the line is a good place
+ );
+ }
+ }
+ newPosition = e.document.validatePosition(newPosition);
+ this.updatePosition(false, newPosition);
+ for (const editor of window.visibleTextEditors) {
+ if (editor.document.fileName === this.curFileName) {
+ editor.setDecorations(this.stickyDecorationType, [new Range(newPosition, newPosition)]);
+ }
+ }
+
+ }
+ }),
commands.registerCommand('_lean.revealPosition', this.revealEditorPosition.bind(this)),
commands.registerCommand('_lean.infoView.pause', () => {
this.stopUpdating();
@@ -116,6 +151,22 @@ export class InfoProvider implements Disposable {
this.stopUpdating();
}
}),
+ commands.registerTextEditorCommand('lean.infoView.toggleStickyPosition', (editor) => {
+ if (this.stickyPosition) {
+ this.stickyPosition = false;
+ for (const ed of window.visibleTextEditors) {
+ if (ed.document.languageId === 'lean') {
+ ed.setDecorations(this.stickyDecorationType, []);
+ }
+ }
+ this.updatePosition(false);
+ } else {
+ this.stickyPosition = true;
+ const pos = editor.selection.active;
+ editor.setDecorations(this.stickyDecorationType, [new Range(pos, pos)]);
+ this.updatePosition(false, pos, editor);
+ }
+ }),
);
if (this.server.alive()) {
this.autoOpen();
@@ -261,7 +312,7 @@ export class InfoProvider implements Disposable {
}
}
- private changePosition() {
+ private changePosition(newStickyValue?: Position) {
if (!window.activeTextEditor ||
!languages.match(this.leanDocs, window.activeTextEditor.document)) {
return;
@@ -270,16 +321,20 @@ export class InfoProvider implements Disposable {
const oldFileName = this.curFileName;
const oldPosition = this.curPosition;
- this.curFileName = window.activeTextEditor.document.fileName;
- this.curPosition = window.activeTextEditor.selection.active;
+ if (newStickyValue) {
+ this.curPosition = newStickyValue;
+ } else if (!this.stickyPosition) {
+ this.curFileName = window.activeTextEditor.document.fileName;
+ this.curPosition = window.activeTextEditor.selection.active;
+ }
return (this.curFileName !== oldFileName || !this.curPosition.isEqual(oldPosition));
}
- private async updatePosition(forceRefresh: boolean) {
+ private async updatePosition(forceRefresh: boolean, newStickyValue?: Position, editor?: TextEditor) {
if (this.stopped) { return; }
- const chPos = this.changePosition();
+ const chPos = this.changePosition(newStickyValue);
if (!chPos && !forceRefresh) {
return;
}