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

Abbreviations / Unicode-Input Improvement Discussion #248

Open
hediet opened this issue Jan 2, 2021 · 2 comments
Open

Abbreviations / Unicode-Input Improvement Discussion #248

hediet opened this issue Jan 2, 2021 · 2 comments

Comments

@hediet
Copy link
Contributor

hediet commented Jan 2, 2021

I have some thoughts about unicode-input improvements that I would like to discuss.
Maybe they can improve working with non-ascii characters.

  1. 99% of the times when I type a1, b1, h2, ..., I mean a₁, b₁, h₂. Maybe such replacements could happen automatically, when a1, b1, ... does not appear anywhere in the current document, but a₁, ... does? Should be easy to implement with an index of all words (i.e. \S+) in the current document. It would be nice if declaration vs usage could be distinguished, but I guess this will only be possible with Lean 4.

  2. I think it might be sensible to replace <-> and -> automatically with their unicode equivalent. (See next point)

  3. Many abbreviations are not prefix-free, i.e. there are abbreviations a and ab such that a is a prefix for ab. This means that when \a has been typed, it could be extended to \ab. Abbreviations that don't have such an extension can be replaced immediately when the last character is inserted. Maybe this can also be implemented for abbreviations that actually have an extension (like \<->)? The replacement would be temporarily and needs to be reverted when another character is added. Maybe some ~300ms timeout could be used to defer replacement of extendable abbreviations.

What do you think?

@bryangingechen
Copy link
Contributor

First, thanks for thinking about the extension! There are certainly lots of improvements that could be made; I think many of the UX decisions up to now have been governed more by ease of implementation / hacks rather than by any principled decisions.

In my opinion, (1) and (2) sound a bit too much like magic to me to have them always on by default, but they seem like reasonable optional settings. (3) sounds interesting; I like the first part of (3) more than the second, but I'd have to test it out to be sure.

A large community of Lean users hangs out at the Lean prover community Zulip, so you may get more comments if you post there.

@hediet
Copy link
Contributor Author

hediet commented Jan 7, 2021

I already implemented the first part of (3) in #240! You can try it out there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants