Go to definition in other isar buffers

[rafaelcgs10]

The main isar-mode buffer allows one to use lsp-find-definition to jump to any hovered term, even those defined in external libraries.

However, the other buffers like lsp-isar-output and lsp-isar-state don't allow this neat feature. This is particularly useful when using commands like find_theorems in which one would like to go to one of the found theorems to check how it was proved.

Are there any plans to extend the lsp functionality to other buffers? Is there any workaround available?

I may be interested in implementing this feature myself if necessary. Would anyone provide any directions for that (e.g. where to look in the code)?

[m-fleury]

I was never motivated enough to implement the function myself… But I welcome contributions!

First some explanation where the information is lost:

1. Isabelle sends all the required information (M-: (setq lsp-print-io t) and check the new buffer for the raw messages):

   <entity ref=\"2404750\" def_line=\"73\" def_offset=\"1656\" def_end_offset=\"1659\" def_file=\"~~/src/HOL/List.thy\" def_id=\"146\" name=\"List.rev\" kind=\"constant\">rev</entity>

2. This information is dropped in the file lsp-isar-output.el

    ('entity
     (setq contents (append (dom-children content) contents)))

To extract the information you can call (dom-attr content 'def_file) or other variants

3. The goal is exported in the function lsp-isar-output-initialize-output-buffer via the variables:

   (list lsp-isar-output-state lsp-isar-output lsp-isar-output-proof-cases-content
             lsp-isar-output-state-deco lsp-isar-output-output-deco)

My guess on how to do it (but there might be better ways!):

1. change the code 'entity extract all relevant information (file + line + offset + which buffer we are currently writing + position of within that buffer) and add all those to an extra variable

2. change lsp-isar-output-recalculate-sync to support one more argument

3. add a backend to xref to support jumps. That backend should read the extra variable to find where to jump.

The few problems I see:

• The file currently is express as ~~, so you need to translate that path to the real file. The AFP might be marked as "$AFP/", but I have not checked.
• I have no idea how xref works
• You have to translate the position from isabelle to the position in emacs

Some more comments for debugging:

• set lsp-isar-output-use-async to nil for debugging (that way you can use message to debug)
• the main file you have to change is https://github.com/m-fleury/isabelle-emacs/blob/Isabelle2022-more-vscode/src/Tools/emacs-lsp/lsp-isar/lsp-isar-output.el#L131