m-fleury / isabelle-emacs

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

Return of the link following issue #58

Closed gh-salt closed 2 years ago

gh-salt commented 2 years ago

The link following issue that we thought we had patched returned with the upgrade to 2021-1! It involves duplicate number of steps in proofs of the open file, and no update of decorations when moving the cursor (as opposed to when inserting text).

gh-salt commented 2 years ago

(lsp--path-to-uri (buffer-file-name)) returns path through symbolic link.

gh-salt commented 2 years ago

(funcall lsp-isar-file-name-follow-links (buffer-file-name)) too

gh-salt commented 2 years ago

(funcall lsp-isar-file-name-unfollow-links (buffer-file-name)) too

gh-salt commented 2 years ago

The function "follow" and "path-to-uri" should return the hard path.

gh-salt commented 2 years ago

Resolved by correcting the regexp of "follow"