10000 Add documentation for interactive highlighting by WhatisRT · Pull Request #7004 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Add documentation for interactive highlighting #7004

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
Merged
merged 1 commit into from
Nov 27, 2023
Merged

Add documentation for interactive highlighting #7004

merged 1 commit into from
Nov 27, 2023

Conversation

WhatisRT
Copy link
Contributor

Interactive highlighting in the emacs mode wasn't documented - this PR is fixing that.

@WhatisRT WhatisRT added the ux: documentation Issues relating to Agda's documentation label Nov 21, 2023
@L-TChen
Copy link
Member
L-TChen commented Nov 21, 2023

Is there any reason to use *non-*interactive highlighting at all? If not, it seems to me that removing the option and using interactive highlighting by default is better.

@UlfNorell
Copy link
Member

The flickering can be a bit distracting when you don't need it, and the implementation is not perfect, sometimes causing interactive highlighting chunks to be left in the buffer.

@omelkonian
Copy link
Contributor

I think we should also include programmatic setting of this options (i.e. the elisp command that you would put in your .emacs file). Describing the UI for setting an option is much more unstable --- it can change with different versions/incarnations of Emacs --- and it seems to me overly verbose to always describe the workflow "customize group RET ...."; currently I see 6 different occurrences of the same workflow (7 including this PR), which could all be subsumed by a single explanation of how to set an agda2 option in general (in a dedicated doc entry).

To sum up, I would ideally prioritize the setq programmatic way to describe each setting and only mention the UI workflow by redirecting to the aforementioned general way of using "customize-group".
If that's too power-user-y for the target audience, at least include a single sentence at the end for the setq way for people with aversion to UI like me :)

@WhatisRT
Copy link
Contributor Author

Since I'll be working on documentation anyway, I can try to include that suggestion as part of the restructuring.

@UlfNorell UlfNorell merged commit 8ede356 into master Nov 27, 2023
@UlfNorell UlfNorell deleted the add-interactive-hl-documentation branch November 27, 2023 08:05
@andreasabel andreasabel mentioned this pull request Feb 7, 2024
Closed
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this pull request Apr 12, 2024
@WhatisRT @JobPetrovcic
Add documentation for interactive highlighting (agda#7004)
5e54c45
@andreasabel andreasabel added this to the 2.6.4.1 milestone Jul 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@UlfNorell UlfNorell UlfNorell approved these changes

Assignees
No one assigned
Labels
ux: documentation Issues relating to Agda's documentation
Projects
None yet
Milestone
2.6.4.1
Development

Successfully merging this pull request may close these issues.
5 participants
@WhatisRT @L-TChen @UlfNorell @omelkonian @andreasabel
0