1, Allow tabs to adjust their size when there are too many tabs. 2, Highlight the words in finding and replacing them

[soarcreator]

I fixed the problem when there are too many tabs on the Editor header. When the remaining space is not enough, all tabs become as small as it is necessary to be to squash into the space.

[facchinm]

Hi @soarcreator , thanks for your contribution!
Did you have the chance to test the beta version of the IDE? It contains a bunch of commits to improve the tabs experience (scrolling tabs + size being adjusted). It still has some bugs (and for this reason it has not been merged in mainline yet).
Would you mind taking a look and helping us to solve the problem for good? Thanks a lot!
The relevant commits are d11c796 5f4daff 17d77d1 d369727

[soarcreator]

Hi, @facchinm
I looked at these commits. d11c796 5f4daff 17d77d1 d369727

Are you trying to change the tab size, depending on whether the tab is selected or not selected?
If so, change my code on the line of 268 in the Editor Header, and use mine.
That line checks if it is necessary to omit the space or not. You can add the extra margin for the selected tab, and draw it in the line of 292.

It looks better to use my commit than these commits because mine has no bug so far.

Additionally, those commits are against the naming rule of other codes. Mine is following the rule.
I don't know why the variables like x_initial, size_selected, and non_selected_tab_size are admitted to exist. All other variables have the different naming rule as far as I know, don't it?

[soarcreator]

New Feature: When finding and replacing the words, all these words are now highlighted yellow for the sake of visibility.

[per1234]

New Feature: When finding and replacing the words, all these words are now highlighted yellow for the sake of visibility.

@soarcreator it would be more appropriate to do that in a separate pull request since it's unrelated to the original proposal here. Create a separate feature branch in your repository for each pull request. Typically you would want to leave the master branch unmodified so that you can pull from the parent repository to that branch but that's not absolutely necessary.

[soarcreator]

@per1234
I agree. I will separate it from this branch if it is undoable.
Thank you.

[soarcreator]

I will close this pull request to separate these two changes.

[per1234]

The way I would do it is:

1. Do an interactive rebase:

   git rebase -i 6da3e5fe20bed2c059050a4ba0a32630b2d33033

2. In the text file that opens, delete the line for the off topic commit and save the file.
3. Do a force push:

   git push -f

You could also use git reset instead of rebasing, but the interactive rebase is a more generally useful tool.

Note that this rewrites the history of your repository, which is not a good practice when other people might be relying on the history not changing and so generally should be avoided. However, in the case of a pull request, rewriting history is fine, and in fact preferred to the alternatives as a way to ensure a clean commit history if the PR is merged. It's probably a good idea to leave a note in the comment thread after rewriting a PR's commit history so that it's clear what happened.

The alternative would be to simply push a new commit that reverts the unwanted commit. It is possible for the repository maintainers to do a "squash merge" of the pull request that will convert multiple commits of the PR into a single commit but this relies on the maintainer actually doing that. In my own PRs, I prefer to take proactive action to ensure the commit history generated by my PR is as I intended, rather than putting the responsibility on the maintainer to remember to do the right thing and figure out how GitHub's squash merge feature works.