Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Why does abort (C-c C-x C-a) remove highlighting from the buffer? #5490

Closed
andreasabel opened this issue Jul 29, 2021 · 0 comments · Fixed by #5491
Closed

Why does abort (C-c C-x C-a) remove highlighting from the buffer? #5490

andreasabel opened this issue Jul 29, 2021 · 0 comments · Fixed by #5491
Assignees
@andreasabel
Labels
ux: emacs Issues relating to the Emacs agda2-mode ux: highlighting Issues relating to syntax highlighting ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Milestone
2.6.2.1

Comments

@andreasabel
Copy link
Member

Why does abort (C-c C-x C-a) remove highlighting from the buffer?

Maybe it shouldn't, as one could still want to jump-to-definition.
@andreasabel andreasabel added ux: emacs Issues relating to the Emacs agda2-mode ux: highlighting Issues relating to syntax highlighting ux: interaction Issues to do with interactive development (holes, case splitting, etc) labels Jul 29, 2021
andreasabel added a commit that referenced this issue Jul 29, 2021
@andreasabel
[ fix #5489 fix #5490 ] Emacs: C-c C-x C-a (abort)
8ae9113 
Change the behavior of 'abort' in the emacs mode:

  - Do not remove highlighting.
    (Can still be useful after abort, e.g. jump to definition).

  - Tell the user that the command was aborted.
@andreasabel andreasabel mentioned this issue Jul 29, 2021
Merged
andreasabel added a commit that referenced this issue Aug 9, 2021
@andreasabel
[ fix #5489 fix #5490 ] Emacs: C-c C-x C-a (abort)
1f75261 
Change the behavior of 'abort' in the emacs mode:

  - Do not remove highlighting.
    (Can still be useful after abort, e.g. jump to definition).

  - Tell the user that the command was aborted.
@andreasabel andreasabel added this to the 2.6.3 milestone Aug 17, 2021
@andreasabel andreasabel self-assigned this Aug 18, 2021
@andreasabel andreasabel modified the milestones: 2.6.3, 2.6.2.1 Aug 18, 2021
andreasabel added a commit that referenced this issue Nov 17, 2021
@andreasabel
[ fix #5489 fix #5490 ] Emacs: C-c C-x C-a (abort)
0340f2a 
Change the behavior of 'abort' in the emacs mode:

  - Do not remove highlighting.
    (Can still be useful after abort, e.g. jump to definition).

  - Tell the user that the command was aborted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
ux: emacs Issues relating to the Emacs agda2-mode ux: highlighting Issues relating to syntax highlighting ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Projects
None yet
Milestone
2.6.2.1
Development

Successfully merging a pull request may close this issue.

[ fix #5489 fix #5490 ] Emacs: C-c C-x C-a (abort) agda/agda
1 participant
@andreasabel