Merge pull request #158 from digama0/sticky

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 <kbd>ctrl</kbd>+<kbd>shift</kbd>+<kbd>enter</kbd> by default)
 * `lean.infoView.displayList`: show all messages for the current file from Lean in the info view window (bound to <kbd>ctrl</kbd>+<kbd>shift</kbd>+<kbd>alt</kbd>+<kbd>enter</kbd> 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 <img src="media/pause.png"> and <img src="media/continue.png"> 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 <kbd>ctrl</kbd>+<kbd>shift</kbd>+<kbd>r</kbd> by default)

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"

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;
         }