search

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
25 stars 5 forks source link

lsp-isar-progress jumps to top when refreshed #3

Closed m-fleury closed 4 years ago

m-fleury commented 4 years ago

https://bitbucket.org/zmaths/isabelle2019-vsce/issues/3/lsp-isar-progress-jumps-to-top-when @gh-salt When the lsp-isar-progress buffer is refreshed, it is printed from the beginning, even when the user is actively looking at this buffer (with active cursor on it).

m-fleury commented 4 years ago

@m-fleury The cursor goes to the line with the selected theory if there is one (unlike before, where it would automatically go back to the first position).

Anyhow, I am surprised that you managed to get a fresh while the cursor is in the progress buffer. Does M-: (fboundp 'json-serialize) return t?

(Patch to come)

m-fleury commented 4 years ago

@m-fleury Should be fixed by f66ab71 (and yes, I got the commit message wrong).

m-fleury commented 4 years ago

@gh-salt M-: (fboundp 'json-serialize) returns nil

But since you fixed it (at least the bug doesn’t occur anymore on my computer) I will close the issue. Thanks!

m-fleury commented 4 years ago

@m-fleury For the record, the new JSON parser in the upcoming emacs (emacs 27) is faster, which makes emacs more stable when running Isabelle.