Rewrite of the abbreviation feature. #240

hediet · 2020-12-30T14:06:27Z

Fixes some bugs in multi-cursor scenarios.
Gets rid of several hacks by introducing a more general system that unifies space/enter and abbreviation-character handling.
Removes now obsolete command "lean.input.convertWithNewline".
Abbreviations are now replaced as soon as possible if the abbreviation is unique.
Adds mobx dependency and makes the abbreviation config observable.

Smart replacing if abbreviation is unique:

Multi-cursor demo:

Except (4) and the bug fixes, no semantics should be changed with this PR.

hediet · 2020-12-30T14:21:07Z

.eslintrc.js

@@ -116,7 +116,7 @@ module.exports = {
        "no-throw-literal": "error",
        "no-trailing-spaces": "error",
        "no-undef-init": "error",
-        "no-underscore-dangle": "error",
+        "no-underscore-dangle": "off",


This setting is turned off to allow fields that can be mutated privately (private _foo: string) but that are readonly publically (get foo(): string { return this._foo; }).

bryangingechen · 2020-12-30T17:46:53Z

package.json

-				"key": "enter",
-				"mac": "enter",
-				"when": "editorTextFocus && editorLangId == lean && lean.input.isActive && !suggestWidgetVisible && !renameInputVisible && !inSnippetMode && !quickFixWidgetVisible && (!vim.active || vim.mode == 'Insert')"
+				"when": "editorTextFocus && !suggestWidgetVisible && editorLangId == lean && lean.input.isActive"


Can you update the README to remove lean.input.convertWithNewline as well?

Maybe you could even add the GIF showing off the abbreviation from your PR comment.

Can you update the README to remove lean.input.convertWithNewline as well?

This is currently not mentioned in the readme - so there is nothing to remove.

Maybe you could even add the GIF showing off the abbreviation from your PR comment.

I would wait until I experimented with the intellisense feature. Also, this GIF is not really meant to document the feature - too much is going on in it.

Whoops, I thought I'd added all options to the README when I revamped it, but I guess I skipped this one. Sorry for the noise!

hediet · 2020-12-31T11:43:59Z

There is still a cursor positioning bug - it happens when typing \ax. Will fix it soon.

src/features/abbreviation/abbreviations.json

* Fixes some bugs in multi-cursor scenarios. * Gets rid of several hacks by introducing a more general system. * Removes now obsolete command "lean.input.convertWithNewline". * Abbreviations are now replaced as soon as possible if the abbreviation is unique. * Adds mobx dependency and makes the abbreviation config observable.

hediet · 2021-01-07T15:46:12Z

There is still a cursor positioning bug - it happens when typing \ax. Will fix it soon.

Fixed!

…ation character.

alexjbest · 2021-01-07T17:58:08Z

Sorry, I haven't tested this myself, but it looks like this changes the behaviour without an option to revert to the original behaviour is that right?

Personally I like the sound of the changes, but I'm a bit worried that we should at least allow people to use the old system if they already have the muscle memory to press tab/enter at the appropriate moment and dont want to change.

hediet · 2021-01-07T18:13:34Z

I will add a setting for that which can disable this behavior!

gebner · 2021-01-13T09:52:59Z

Thanks for putting effort into improving the input mode! Some comments:

The new directory structure is very "enterprisey".

Please keep the translations.json file where it is right now, in the root directory. Other projects rely on this location.
Also, please avoid deeply-nested directory structures like src/features/abbreviation/AbbreviationRewriterFeature/AbbreviationRewriterFeature.ts. Please make just a single directory src/abbreviation and put everything in there.

Also feel free to put more functions/classes in a single file, this is not java.

Please run eslint on the files (I think there's something wrong with npm run lint though, because it doesn't lint the new files...).

What is the reason to add a new Range type (i.e. why is vscode.Range not enough)?

Finally, please add the setting that Alex mentioned.

hediet · 2021-01-13T10:19:27Z

What is the reason to add a new Range type (i.e. why is vscode.Range not enough)?

Like the docs say: Range is offset/length based in contrast to vscode.Range which is line/column based.

It is way easier to get correctness with offset based datastructures, as you would need to detect line breaks in text that got inserted. This is the reason for some bugs in the current implementation, if the multiple cursors are added to the same line.

Please keep the translations.json file where it is right now, in the root directory. Other projects rely on this location.

Can do that, but I still find it confusing that it is called translations.json.
Also, if other projects depend on it, this should be documented. I added some <> -> <$CURSOR> abbreviations where the cursor is moved to $CURSOR after rewriting. I guess other projects might not like that and thus this needs to be changed.

Also, please avoid deeply-nested directory structures like src/features/abbreviation/AbbreviationRewriterFeature/AbbreviationRewriterFeature.ts. Please make just a single directory src/abbreviation and put everything in there.

I also can do that, but personally, I'm against it. The "abbreviation" feature consists of several subfeatures - the rewriting, the hover-provider and maybe someday an autocompletion. The rewrite feature has these four entities (AbbreviationRewriter which is per editor, AbbreviationRewriterFeature which is the thing that instantiates all the rewriters, Range which is a util thing and TrackedAbbreviation which is per tracked abbreviation in an editor) - I think they deserve a separate folder.

Also feel free to put more functions/classes in a single file, this is not java.

I used to put many things into single files as it has been done in input.ts. But I find it very hard to get an overview of input.ts, as I need to scroll over all these details to figure out the larger picture. Btw. in Java you can also put multiple non-public classes into a single file! It is just a convention that you shouldn't do it and I think this is often for a good reason. I certainly agree that it does not make much sense for files with less than ~20 lines of code (as it sometimes happens for java), but this is not the case here.

Please run eslint on the files (I think there's something wrong with npm run lint though, because it doesn't lint the new files...).

This is strange, I can try to fix that. I also highly recommend to setup prettier for formatting, enable strict mode and lift some eslint/tslint rules. Currently, tslint is doing stuff that other tools can do better.

Finally, please add the setting that Alex mentioned.

Will do that.

gebner · 2021-01-13T10:58:14Z

It is way easier to get correctness with offset based datastructures, as you would need to detect line breaks in text that got inserted. This is the reason for some bugs in the current implementation, if the multiple cursors are added to the same line.

This makes sense!

Also, if other projects depend on it, this should be documented. I added some <> -> <$CURSOR> abbreviations where the cursor is moved to $CURSOR after rewriting. I guess other projects might not like that and thus this needs to be changed.

Good point! Feel free to rename it to abbreviations.json then if the format changes. But I'd still prefer to keep it in the root directory (where it is more visible).

Also, please avoid deeply-nested directory structures like src/features/abbreviation/AbbreviationRewriterFeature/AbbreviationRewriterFeature.ts.
I also can do that, but personally, I'm against it. The "abbreviation" feature consists of several subfeatures - the rewriting, the hover-provider and maybe someday an autocompletion. The rewrite feature has these four entities [...] - I think they deserve a separate folder.

The overriding principle here is consistency with the rest of the codebase, which doesn't use directory hierarchies either.

And I'm not even against subdirectories. I like src/abbreviation, since there are now a lot of files for this features and it's great that they're grouped together. src/abbreviation/rewriter/Range.ts would still be ok. But repeating the name three times in the path is just too much:
src/features/abbreviation/AbbreviationRewriterFeature/AbbreviationRewriterFeature.ts

The features directory is superfluous, it only contains a single entry. The word "abbreviation" is repeated three times. And the even longer "AbbreviationRewriterFeature" is repeated twice.

This is strange, I can try to fix that. I also highly recommend to setup prettier for formatting, enable strict mode and lift some eslint/tslint rules. Currently, tslint is doing stuff that other tools can do better.

Feel free to add prettier if you'd like. (But in a different PR please.)

hediet · 2021-01-13T11:33:38Z

The features directory is superfluous

It very much is (currently)! But I can only recommend separating feature code from core/infrastructure code.
For me, a feature is some clear unit that you could delete and after deletion, you only need to touch like 1-5 lines of code to make the entire project work again (without the feature).
extension.ts, server.ts, shared.ts, util.ts, ... are all no features, while completion.ts, statusbar.ts, infoview.ts, ... (I guess) are.
Organizing code into features makes it very easy to identify the code you need to touch for implementing a certain effect.
The current src dir has 25 files which makes linear search increasingly difficult. Putting a decision tree in front of those files might make that much easier.

I'll remove the features folder from this PR, but I can really recommend this structure.

But repeating the name three times in the path is just too much:

I understand your point and I will change it, but there was some reasoning behind chosing those names. If you configure the indentation in VS Code of nested folders, long names are not problematic anymore.
My naming scheme (and the one we use where I work) is the following:

kebab-case-name(.ts)? if the item refers to some general concept.
UpperCamelCase(.ts)? if the item refers to a main symbol of that name.
The folder AbbreviationRewriterFeature refers to the class AbbreviationRewriterFeature as being the most important symbol in that folder.

Feel free to add prettier if you'd like. (But in a different PR please.)

I will!

But I'd still prefer to keep it in the root directory (where it is more visible).

There was also a technical change that required me to move it - I changed the code to bundle the json file directly as source, rather than loading it as file dynamically.
My change has the advantage that the compilation process checks the file path (and requires no dependency to load-json-file), while the dynamic import does not do that.

However, if abbreviations.json is now treated as source file, typescript puts its restrictions on it:

File 's:/dev/contrib/vscode-lean/abbreviations.json' is not under 'rootDir' 's:/dev/contrib/vscode-lean/src'. 'rootDir' is expected to contain all source files.ts(6059)

I can try to fix that, even though I guess I need to fallback to the mechanism used in the current master.

gebner · 2021-01-13T11:54:19Z

There was also a technical change that required me to move it - I changed the code to bundle the json file directly as source, rather than loading it as file dynamically.

Ah, if there's a good reason then that's fine too. We have quite a few users though that contribute to the file but don't develop the extension, so it'd be great if it was still easy to find (from the github page).

Organizing code into features makes it very easy to identify the code you need to touch for implementing a certain effect.
The current src dir has 25 files which makes linear search increasingly difficult. Putting a decision tree in front of those files might make that much easier.

I agree, and that's why I said that a new directory for the abbreviations feature is a great idea.

Different projects have different organization styles. It is better to be consistent within a project than to conform (partially) to a style guide, no matter how well-thought out it may be. The optimal organization also depends on the size of a project, a 10-line script requiring a different setup than a 100k line project.

I am sure that at your company all new repositories conform to these style guides, and this is great for consistency and uniformity, and makes it easier for new people to get started on a project. But this is not your company, and following such an elaborate style guide can even be detrimental since nobody here is familiar with it, negating some of the advantages. This holds doubly if the style is only followed partially, for a single feature.

hediet · 2021-01-13T11:59:21Z

This holds doubly if the style is only followed partially, for a single feature.

Very true and I will change these things in this PR to be more consistent with the existing code.

Nonetheless, I think with 25 files in the src folder on master, it might already make sense to organize them in feature-like folders. This is independent of this PR though.

hediet · 2021-01-16T15:26:39Z

I got rid of the features folder
renamed the folders to a shorter name
ran eslint
added the setting key lean.input.eagerReplacementEnabled that can be used to turn off that feature (on by default).
added some docs for abbreviation.json

…-feature-rewrite

hediet · 2021-01-19T12:11:13Z

🎉

eric-wieser · 2021-05-10T11:11:05Z

src/abbreviation/rewriter/AbbreviationRewriter.ts

+		// Wait for VS Code to trigger `onDidChangeTextEditorSelection`
+		await waitForNextTick();


My understanding is that this timeout is non-deterministic, and is the cause of the "sometimes the replacement doesn't happen" bug. It happens more when lean is busy.

"sometimes the replacement doesn't happen"

This happens if the user changes the text buffer after the replacement is issued but before it is committed. This is unavoidable, it can only be made less likely to happen (I only learned recently about this, sorry for not having taken this into account when I wrote that code).

Internally, VS Code has a version number per text document that is incremented on every edit. Edits are sent asynchronously to the extensions and if an extension issues an (async) text modification it is only applied if the version of the target document has not changed in the meantime.

waitForNextTick makes it more likely that a user can change the text buffer before the extension can commit the text modification.

However, waitForNextTick is also required to position the cursor correctly after the replacment has been committed.

Your fix is a good workaround, but maybe the extension can actually try a second time to perform this replacement. Sadly (afaik) VS Code does not allow transactional updates that involve text and cursor modification.

hediet force-pushed the hediet/abbreviation-feature-rewrite branch from 430a49f to c564341 Compare December 30, 2020 14:19

hediet commented Dec 30, 2020

View reviewed changes

This was referenced Dec 30, 2020

Intellisense For Abbreviations #244

Open

Live Preview Of Abbreviation Symbols #245

Open

bryangingechen reviewed Dec 30, 2020

View reviewed changes

ocfnash reviewed Jan 4, 2021

View reviewed changes

src/features/abbreviation/abbreviations.json Outdated Show resolved Hide resolved

hediet force-pushed the hediet/abbreviation-feature-rewrite branch 2 times, most recently from 67e5d37 to f5fcac6 Compare January 7, 2021 15:44

hediet added 2 commits January 7, 2021 16:45

Fixed selection positioning bug.

ce67fb0

hediet force-pushed the hediet/abbreviation-feature-rewrite branch from f5fcac6 to ce67fb0 Compare January 7, 2021 15:45

hediet added 2 commits January 7, 2021 17:01

Fixes selection correction after expanding f<<>>.

62af8a5

Fixes bug that happens when an abbreviation is ended with the abbrevi…

c0d9523

…ation character.

hediet mentioned this pull request Jan 7, 2021

Abbreviations / Unicode-Input Improvement Discussion #248

Open

hediet added 2 commits January 16, 2021 16:19

Fixes issues from PR.

9b29d60

Fixes formatting in extension.ts.

53fa20a

Merge remote-tracking branch 'origin/master' into hediet/abbreviation…

5f534ae

…-feature-rewrite

gebner merged commit e4c3b27 into leanprover:master Jan 19, 2021

eric-wieser reviewed May 10, 2021

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rewrite of the abbreviation feature. #240

Rewrite of the abbreviation feature. #240

hediet commented Dec 30, 2020 •

edited

Loading

hediet Dec 30, 2020 •

edited

Loading

bryangingechen Dec 30, 2020

hediet Dec 30, 2020

bryangingechen Dec 30, 2020

hediet commented Dec 31, 2020

hediet commented Jan 7, 2021

alexjbest commented Jan 7, 2021

hediet commented Jan 7, 2021

gebner commented Jan 13, 2021

hediet commented Jan 13, 2021 •

edited

Loading

gebner commented Jan 13, 2021

hediet commented Jan 13, 2021

gebner commented Jan 13, 2021

hediet commented Jan 13, 2021 •

edited

Loading

hediet commented Jan 16, 2021

hediet commented Jan 19, 2021

eric-wieser May 10, 2021

hediet May 10, 2021 •

edited

Loading

		// Wait for VS Code to trigger `onDidChangeTextEditorSelection`
		await waitForNextTick();

Rewrite of the abbreviation feature. #240

Rewrite of the abbreviation feature. #240

Conversation

hediet commented Dec 30, 2020 • edited Loading

hediet Dec 30, 2020 • edited Loading

Choose a reason for hiding this comment

bryangingechen Dec 30, 2020

Choose a reason for hiding this comment

hediet Dec 30, 2020

Choose a reason for hiding this comment

bryangingechen Dec 30, 2020

Choose a reason for hiding this comment

hediet commented Dec 31, 2020

hediet commented Jan 7, 2021

alexjbest commented Jan 7, 2021

hediet commented Jan 7, 2021

gebner commented Jan 13, 2021

hediet commented Jan 13, 2021 • edited Loading

gebner commented Jan 13, 2021

hediet commented Jan 13, 2021

gebner commented Jan 13, 2021

hediet commented Jan 13, 2021 • edited Loading

hediet commented Jan 16, 2021

hediet commented Jan 19, 2021

eric-wieser May 10, 2021

Choose a reason for hiding this comment

hediet May 10, 2021 • edited Loading

Choose a reason for hiding this comment

hediet commented Dec 30, 2020 •

edited

Loading

hediet Dec 30, 2020 •

edited

Loading

hediet commented Jan 13, 2021 •

edited

Loading

hediet commented Jan 13, 2021 •

edited

Loading

hediet May 10, 2021 •

edited

Loading