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

Remove ' and add ⟨⟩ in lean autopairs #10688

Merged
merged 1 commit into from
May 5, 2024

Conversation

ashl3y-v
Copy link
Contributor

@ashl3y-v ashl3y-v commented May 5, 2024

Add an auto-pairs section to the lean configuration with ⟨⟩ and without ''
Rationale: ⟨⟩ is very commonly used for pattern matching and essentially always used in a pair, and ' is also very commonly used for denoting "prime" almost never used in a pair. If only using one ' the pairing isn't an issue, but when trying to type two, the pairing creates ''' instead, and the same issue is present when trying to type four, etc.
There were issues with 3 byte characters for pairs but they were fixed: #3964 and #3946.
Sorry if there are any issues, I'm new to this.

@pascalkuthe pascalkuthe added the S-waiting-on-review Status: Awaiting review from a maintainer. label May 5, 2024
@archseer archseer merged commit 6181899 into helix-editor:master May 5, 2024
6 checks passed
Vulpesx pushed a commit to Vulpesx/helix that referenced this pull request Jun 7, 2024
Chirikumbrah pushed a commit to Chirikumbrah/helix that referenced this pull request Jun 15, 2024
smortime pushed a commit to smortime/helix that referenced this pull request Jul 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
S-waiting-on-review Status: Awaiting review from a maintainer.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Strange behaviour when auto-pairing Unicode brackets
3 participants