Pinned selections are not properly anchored

[lovettchris]

Repro:

1. Open a new .lean file and add this to the top of the file:
   #eval 123
2. Pin that, so you should see this:
   
3. Go to the end of the line and type ENTER

Actual: infoview shows this error

Expected: pinned selections should be properly anchored.

The bug appears to be in infos.tsx where it is listening to textDocument/didChange and trying up update the pin positions from the change information in the DidChangeTextDocumentParams but the code is buggy and very incomplete. Notice in this case the code has moved the pin to line 2 character 9, which is a position that doesn't exist in the document - hence the error.

What we really need is a proper "anchored selection", or what some people call a Tracked Selection that moves with prior code edits and can also be "deleted" if the user deletes a range of text including this tracked selection position. Then the infoview should listen to "move" and "delete" events on this tracked selection and update the pin positions accordingly. So I propose we put all this tracking in the editor extension, and simplify the infoview code so it is simply using a new InfoViewApi "createTrackedSelection" or something, and a useClientNotificationState to listen to changes on these tracked selections.

[lovettchris]

Something like this:

import { RangeHelpers } from '@lean4/infoview/dist/infoview/util';
import {
    Disposable, TextEditor
} from 'vscode';

import * as ls from 'vscode-languageserver-protocol'

export class Bookmarks implements Disposable
{
    stickyPositions: ls.Location[];

    constructor() {
        this.stickyPositions= [];
    }

    addBookmark(editor: TextEditor) : void {
        if (!editor) return;
        const uri = editor.document.uri;
        const selection = editor.selection;
        const loc : ls.Location = {
            uri: uri.toString(),
            range: {
                start: selection.start,
                end: selection.end
            }
        };

        this.stickyPositions.push(loc);
    }

    onChange(change: ls.DidChangeTextDocumentParams){
        const uri = change.textDocument.uri;
        for (const loc of this.stickyPositions){
            if (loc.uri === uri){
                for (const e of change.contentChanges){
                    if (ls.TextDocumentContentChangeEvent.isIncremental(e)) {
                        const range = e.range;
                        const text = e.text;
                        const end = range.end;
                        const start = range.start;
                        if (text === ''){
                            console.log(`delete from ${start.line},${start.character} to ${end.line},${end.character}`)
                        } else if (start.line === end.line && start.character === end.character) {
                            // this is a pure insert
                            console.log(`insert text from ${start.line},${start.character} to ${end.line},${end.character}`)
                        } else {
                            // if range is non-empty then it is replacing the range with "text".
                            // and this "replace" operation could have encompassed a pin in which case we
                            // probably should delete that pin.
                            console.log(`replace from ${start.line},${start.character} to ${end.line},${end.character}`)
                        }
                    } else if (ls.TextDocumentContentChangeEvent.isFull(e)){
                        // full replacement of the document kind of blows away all pins then!
                        const text = e.text;
                        console.log('full replace')
                    }
                }
            }
        }
    }

    onClosed(closed: ls.DidCloseTextDocumentParams){
        this.stickyPositions = this.stickyPositions.filter(i => i.uri !== closed.textDocument.uri);
    }

    dispose(): void {
        this.stickyPositions = [];
    }
}

[Vtec234]

@lovettchris thanks a bunch for the repro, it was very helpful. That said, I disagree that the proper fix here is to do this kind of major refactor. The code would still be as buggy, just in a different place :) And we would have to increase the infoview API surface. I attempted a fix in the linked PR which also resolves an old TODO about correct character calculations, could you please try if it works?

So I propose we put all this tracking in the editor extension, and simplify the infoview code so it is simply using a new InfoViewApi "createTrackedSelection" or something

To elaborate, the reason I am resistant to this kind of change besides it being an IMO unnecessary refactor is that last summer I actually moved this code out of the extension and into the infoview. You could argue quite convincingly that that also was an unnecessary refactor 😅. However, it had a purpose - to handle as much stuff as we can in the infoview and leave the extension code minimal, so that other editors can embed the infoview without reimplementing all this. This "other editors embedding infoview" point is currently vaporware, but my insistence on it has real technical implications. That said, there seems to be interest at least from the Emacs folks in making this work. I think in either case we should figure out whether we are supporting this and keeping the infoview editor-independent, or whether it's okay to move its parts to the VSCode extension whenever convenient and therefore make those parts dependent on VSCode. After figuring this out let's commit to it, because it matters a lot to the design.

[lovettchris]

Well the bookmarks implementation could live in either place actually, but in order to do anchored bookmarks properly we are missing a vscode feature, see my bugbug in bookmarks.ts and my question to vscode about how to do that properly. Usually anchors are provided by the "editor" (I assume emacs already has it, Visual Studio certainly does). But I can't find it in vscode yet... So in emacs how are they done, I could imagine an editor specific custom "anchoredselection" object hiding inside the "bookmark" that is then sent to the infoview and auto-updates so the hacky code in infos.tsx all goes away. Annoyingly all the top "bookmarks" extensions that plug into VSCode and work, have hidden their real implementation in private github submodules!

[lovettchris]

I've updated bookmarks.ts so it now properly computes the "before" text using it's own ugly cache of original buffer text and this works nicely. I can now do all kinds of crazy edits and the book mark is recomputed correctly, for example, take this original code:

/-
This is an eval statement
-/
#eval 123

and put a pin at the end of the eval, then select from the beginning of the file to after the string #eval but not the 123 part, and paste the following:

def square (x:Nat) :=
  x * x


#eval (square 5) *

The bookmark computes the pin should now be at line 5, character 21. But our current pin remains at 5:9. Similarly, if I do a replace that adds a bunch of lines our current pin jumps to this the location 9,9999 and prints a big red message.

[lovettchris]

This is what the new EditorApi additions would be:

  /** Adds a bookmark that updates its position automatically when prior edits are made in the document,
   * and returns an "id" for this bookmark that you can correlate with bookmark updates sent to the InfoviewApi. */
  addBookmark(pos: TextDocumentPositionParams): Promise<string>;
  /** Removes a bookmark that was added via addBookmark. */
  removeBookmark(id: string): Promise<void>;

This is what the new InfoViewApi additions could be:

  /**
   * Notifies the infoview when a given bookmark (created via EditorApi createBookmark) has moved.
   * @param id The id of the bookmark
   * @param pos The new position of the bookmark.
   */
  bookmarkChanged(id: string, pos: TextDocumentPositionParams): Promise<void>;

  /**
   * Notifies the infoview that the given bookmark is no longer valid.
   * @param id The id of the bookmark that was removed.
   */
  bookmarkRemoved(id: string): Promise<void>;

[lovettchris]

@Vtec234 , well just for fun I completed the thought experiment and it fixes the bugs listed here.

See #202

[Vtec234]

put a pin at the end of the eval, then select from the beginning of the file to after the string #eval but not the 123 part, and paste the following:

Thanks for the example, it is also handled correctly in #201.

well just for fun I completed the thought experiment and it fixes the bugs listed here.

Thanks for experimenting with this. As I wrote though, I don't see any reason to do this large refactor when the issue is also fixed by a few small changes to the algorithm. Could you explain why you believe that the code in infos.tsx is hacky and we need the whole bookmark API to track pins properly?

[lovettchris]

I also see from your code that what I was doing in bookmarks.ts was unnecessary, we can indeed compute everything we need from the contentChanges.range information. So my bookmarks.ts code is now simpler and more similar to your code in #201. So I guess the only remaining question is whether bookmarks are harder to implement in other editors that might have more sophisticated editing operations, or whether a more general bookmark would be useful anyway for other future lean features. But we can table that discussion for now since your PR seems to fix the bugs mentioned here. Just need to make sure it passes my new improved test: #204

[gebner]

To elaborate, the reason I am resistant to this kind of change besides it being an IMO unnecessary refactor is that last summer I actually moved this code out of the extension and into the infoview. You could argue quite convincingly that that also was an unnecessary refactor sweat_smile. However, it had a purpose - to handle as much stuff as we can in the infoview and leave the extension code minimal, so that other editors can embed the infoview without reimplementing all this. This "other editors embedding infoview" point is currently vaporware, but my insistence on it has real technical implications.

I think that "other editors" is a big red herring here. Chris' bookmark API is trivial to implement in neovim (using extmarks), and emacs (using markers). I think it's only vscode where we need to implement this ourselves. These editor APIs are also significantly more robust than intercepting LSP notifications (which may not even be easily possible in neovim). For example, the LSP interception won't work if you temporarily disable LSP checking, or if the editor uses full synchronization.

That said, there seems to be interest at least from the Emacs folks in making this work. I think in either case we should figure out whether we are supporting this and keeping the infoview editor-independent, or whether it's okay to move its parts to the VSCode extension whenever convenient and therefore make those parts dependent on VSCode.

I don't think that moving the API boundary here makes a difference for editor-independence. If anything, removing LSP interception makes it easier to implement in other editors.

[Vtec234]

If anything, removing LSP interception makes it easier to implement in other editors.

Restricting attention to just neovim, from a quick skim of the docs it does look like there is no generic "on notification" callback registration. Are you planning to spawn a webview from neovim that's separate from the current text-based lean.nvim implementation? If so, could you please make an issue about supporting that? If we want to go this route, we'd have to remove all uses of subscribeClientNotifications and subscribeServerNotifications, and rm them from the infoview API.

I think that "other editors" is a big red herring here.

Yes, it's my bad for mentioning it in the first place. This issue really is just about pin positions, and what I was trying to say is "we can fix this with a small local change, so I'd rather not do a larger bookmark refactor, and also the proposed refactor has implications for editor-independence". I see that I was wrong about the last part when it comes to Neovim but as far as I can tell, the actual issue is fixed now.

[gebner]

Are you planning to spawn a webview from neovim that's separate from the current text-based lean.nvim implementation?

Good question. Right now there doesn't seem to be any neovim gui that supports webviews. Maybe uivonim will at some point, but that frontend doesn't seem to very active.

I've also thought about just starting a web server and opening the infoview in a browser. But all of that is very low priority, at least until people build graphical widgets we can't live without, because we already have text-based interactive expressions.

we can fix this with a small local change, so I'd rather not do a larger bookmark refactor

Completely agreed on that.

[lovettchris]

These editor APIs are also significantly more robust than intercepting LSP notifications
If anything, removing LSP interception makes it easier to implement in other editors.

Gabriel, this is why I was moving the bookmarks to the extension, so infoview doesn't need tu ise LSP notifications. Then you can hook up a real editor's implementation of bookmarks there and only the vscode version would have it's own implementation (until vscode provides something similar - which they may actually do because they are getting a lot of requests for it).