Skip to content

Conversation

@anarchoisomorphism
Copy link

Recently a commit introduced a debouncer to fix an issue with an overly eager checker rubber-banding the editor if you typed too quickly. This commit adds a DebounceTime configuration option, defaulting to 250ms.

CCing @DikieDick as per request. I haven't done any testing on this feature apart from building and unit tests, please let me know how to load this onto VSC so I could make sure everything checks out 🙇‍♀️

Recently a commit introduced a debouncer to fix an issue with an overly
eager checker rubber-banding the editor if you typed too quickly. This
commit adds a DebounceTime configuration option, defaulting to 250ms.
@DikieDick
Copy link
Contributor

Thank you for reaching out! It is very nice to see that you took the time to implement this.

please let me know how to load this onto VSC so I could make sure everything checks out 🙇‍♀️

You can open the project in VSCode/Codium and press F5 (or use Run > Start Debugging) to run the extension in extension developer mode.

The instructions under developer-resources/developer_instructions.md contain more information.

If you need any help with setting up the development environment, feel free to ask.

@DikieDick
Copy link
Contributor

Before merging this PR, I think it is important that you do indeed test out the changes locally and see how it behaves.

Moreover, I have the following suggestions:

  • In waterproof-editor, the editor part of the project, there is a similar debounce delay. The default there is 750ms, therefore I'd suggest we make the default here 750 as well.

  • I think that the setting may be better placed under the "Editor Experience" category, instead of "Diagnostic Reporting". The description of the setting should also better reflect what exactly the timeout delays in my opinion. In this case it adds extra delay between the moment the user stops typing and the input area bar becoming green (in the case of a correct proof).

Let me know whether you like to adopt the above suggestions yourself or if I (at any point) should take over.

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

Successfully merging this pull request may close these issues.

2 participants