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.

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

feat: "Try this:" custom code action title #466

Merged

Conversation

thorimur
Copy link
Contributor

@thorimur thorimur commented Dec 16, 2023

Currently, the code action title in the lightbulb menu is hardcoded to Try this: <prettyPrintedSuggestionText>. This needs to be customized in various cases, such as teaching in non-English languages. This PR:

  • Adds a field toCodeActionTitle? : Option (String -> String) to Suggestion, which, if provided, can be applied to the pretty-printed suggestion text and transform it as desired (note that this application occurs prior to encoding, so we only pass the resulting code action title String, if any, to the Json version of the Suggestion structure; note also that we don't want to pretty-print twice, so we take in the pretty-printed String as an argument instead of the SuggestionText itself)
  • Adds an argument codeActionPrefix? : Option String := none to addSuggestions to conveniently provide a default code action title prefix to use for all elements in an Array Suggestion which do not have a nontrivial toCodeAction? value.

See zulip for the feature request and discussion on the choice of default behavior.

@thorimur
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Dec 16, 2023
@joehendrix joehendrix added will-merge-soon PR will be merged soon. Any concerns should be raised quickly. and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Dec 20, 2023
@joehendrix joehendrix merged commit 455498d into leanprover-community:main Dec 20, 2023
1 check passed
semorrison added a commit that referenced this pull request Dec 21, 2023
commit 74d2899
Author: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date:   Sun Dec 17 01:56:41 2023 +0100

    chore: set toolchain

commit 3f88f41
Author: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date:   Sun Dec 17 01:52:45 2023 +0100

    feat: adapt TryThis
Revert "feat: "Try this:" custom code action title (#466)"

This reverts commit 455498d.
semorrison added a commit that referenced this pull request Dec 21, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants