emacs tools

Stream: general

[Simon Hudon]

Is it possible in emacs lisp to use lean-server-session-send-command to get the text of a definition? Failing that, is it possible to use it with the command 'info to get the line info of the next command in the file that contains it? I'm trying to create a command to display the definition of the symbol the cursor is currently on.

[Sebastian Ullrich]

No, I can't think of any way to do that

[Simon Hudon]

What I ended up doing is use the list of keywords in lean-syntax and only keep the ones that are commands, use lean-find-definition to find the location of the definition and re-search-forward to find the next command. That's pretty primitive because it doesn't account for user command but it might just be good enough.

[Sebastian Ullrich]

Good enough I guess :)

[Simon Hudon]

I'm wondering if it would be more useful to just go with find definition and have an option to go back. What do you think? The easiest way to do it is provide one slot memory for finding definition but it would be nicer to have many slots. I just don't want it to grow without bounds.

[Reid Barton]

How about setting the mark to the old location if the definition is in the same file?

[Simon Hudon]

What does that solve?

[Reid Barton]

then you can C-x C-x to go back

[Reid Barton]

for example, isearch (C-s) does this

[Simon Hudon]

Ah I see! But then when you go to another file, you have a different shortcut than when you stay in the same file

[Reid Barton]

Apparently there's also C-x C-SPC which will pop marks off a global stack, between files

[Reid Barton]

So that would always work as a "go back" key

[Reid Barton]

https://stackoverflow.com/questions/4918707/in-emacs-how-to-go-back-to-previous-line-position-after-using-semantic-jump-to

[Simon Hudon]

Nice! So you suggest that in lean-find-definition (which is called when you press M-.) I first push the mark and then set the mark to (point) and then the user will simply have access to those features?

[Simon Hudon]

Is there a limit to the number of slots on that stack?

[Reid Barton]

I don't know. I just found out the limit is more than one :simple_smile:

[Reid Barton]

I think you just need to call (push-mark) before doing the navigation

[Reid Barton]

mark-ring-max is a variable defined in ‘simple.el’.
Its value is 16

Documentation:
Maximum size of mark ring.  Start discarding off end if gets this big.

[Simon Hudon]

I think you just need to call (push-mark) before doing the navigation

Inside of lean-mode or as a user of lean-mode?

[Reid Barton]

lean-find-definition should call it (I guess, haven't looked at the code)

[Reid Barton]

Hmm. I see there is already this, in lean-find-definition-cont

(cl-defun lean-find-definition-cont (&key file line column)
  (when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack))
...

[Simon Hudon]

This is so nice! It's working very well!

[Simon Hudon]

Thanks!

[Simon Hudon]

I can PR it if you'd like to have it too

[Reid Barton]

Yes please

[Reid Barton]

I've been wanting this feature too, but the mark thing just occurred to me now

[Reid Barton]

It looks like maybe M-, already does the same thing? but I have that mapped to autocomplete

[Simon Hudon]

You're right! I undid my changes and M-. M-. M-, M-, brings me back to the beginning. It looks like my pull request will be the empty set. I hope it's approved!