cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
354 stars 29 forks source link

emacs TAGS #198

Open spitters opened 6 years ago

spitters commented 6 years ago

M-. jumps to definition. Looking at the behavior of emacs TAGS, I would expect M-* to bring me back. Perhaps one could add such a key-binding?

cpitclaudel commented 6 years ago

I'm not familiar with M-*, though I do see a reference to it in the news for Emacs 20. When I use M-. to jump to a tags file, pressing M- complains about it being undefined. Do you know where `M-` is defined?

In any case, I think the standard command for this is now M-,, which does work with company-coq on emacs 25+. Can you try that and confirm that it works?

spitters commented 6 years ago

After M-. on "list", I get taken to Init/Datatypes.v

M-, gives "marker stack empty"

Here are the TAGS keybindings:

https://www.emacswiki.org/emacs/EmacsTags#toc1

On Mon, May 21, 2018 at 9:06 PM, Clément Pit-Claudel < notifications@github.com> wrote:

I'm not familiar with M-, though I do see a reference to it in the news for Emacs 20. When I use M-. to jump to a tags file, pressing M- complains about it being undefined. Do you know where M-* is defined?

In any case, I think the standard command for this is now M-,, which does work with company-coq on emacs 25+. Can you try that and confirm that it works?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/198#issuecomment-390751494, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zizKlmktIN3MPWSYbC6gdwxzbnnFks5t0xAdgaJpZM4UHSHq .

cpitclaudel commented 6 years ago

Thanks. Is updating to a newer Emacs an option?

spitters commented 6 years ago

I'm on Ubuntu 18.04:

emacs --version GNU Emacs 25.2.2

On Mon, May 21, 2018 at 9:21 PM, Clément Pit-Claudel < notifications@github.com> wrote:

Thanks. Is updating to a newer Emacs an option?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/198#issuecomment-390755423, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2ztt6U720ijEZWib4GPXXmLN72Plcks5t0xO_gaJpZM4UHSHq .

cpitclaudel commented 6 years ago

Hmm. Thanks. Let me check then.

cpitclaudel commented 6 years ago

Surprising. Here on Emacs 25.2, M-* says undefined and M-, jumps back. I tried in a C file with an appropriate tags file.

What does M-: (fboundp 'xref-push-marker-stack) return? What about M-: (require 'xref)? Does that raise an error? If not, does M-. followed by M-, work after this require?

spitters commented 6 years ago

What does M-: (fboundp 'xref-push-marker-stack) return? t

What about M-: (require 'xref)? xref

does M-. followed by M-, work after this require? Still the same error

On Mon, May 21, 2018 at 9:41 PM, Clément Pit-Claudel < notifications@github.com> wrote:

Surprising. Here on Emacs 25.2, M-* says undefined and M-, jumps back. I tried in a C file with an appropriate tags file.

What does M-: (fboundp 'xref-push-marker-stack) return? What about M-: (require 'xref)? Does that raise an error? If not, does M-. followed by M-, work after this require?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/198#issuecomment-390760371, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zlGyRSzeLBtHDppwGsv9JKK0Hi3xks5t0xiEgaJpZM4UHSHq .

cpitclaudel commented 6 years ago

Snap. Thanks for giving it a try.

Just to understand better, can you tell me what C-h k M-. returns in a C buffer, or some other language where you use tags? What about C-h k M-*? Finally, can you try M-x where-is RET xref-pop-marker-stack, too?