Stream: Proof General users

Topic: Go back from "jump-to-definition"

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 12:12):

Company-coq lets you jump to definition with M-. (or with , g g in spacemacs's coq layer), but how do you jump back? I don't see M-, working... Probably spacemacs interferes, but docs don't seem to mention it?

view this post on Zulip Ana de Almeida Borges (Mar 28 2022 at 13:50):

I don't know the Company-coq way, but if you happen to use vim keybindings, you can use Ctrl+o to jump back to where you were (and Ctrl+i to more forward).

view this post on Zulip MackieLoeffel (Mar 29 2022 at 06:33):

I think this M-. uses the standard mark ring infrastructure to save the previous location. So you can jump back with pop-global-mark. For me, this is bound to C-x C-@.

Last updated: Oct 13 2024 at 01:02 UTC