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.

Sign up for GitHub

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

Jump to bottom

Support different tab heights #192153

Merged
merged 11 commits into from
Sep 6, 2023
Merged

Support different tab heights #192153

merged 11 commits into from
Sep 6, 2023

Conversation

benibenj
Copy link
Contributor

@benibenj benibenj commented Sep 4, 2023 •
edited
Loading

Feature Request: #42253

Added setting tabHeight which allows to change the height of the editor tab.

Supported options:

  • normal: Default tab height
  • compact: Same height as breadcrumbs

@benibenj benibenj added this to the September 2023 milestone Sep 4, 2023
@benibenj benibenj self-assigned this Sep 4, 2023
bpasero
bpasero requested changes Sep 5, 2023
View reviewed changes
Copy link
Member

@bpasero bpasero left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very cool already, left some thoughts 👏

src/vs/workbench/browser/workbench.contribution.ts Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/media/titlecontrol.css Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/tabsTitleControl.ts Outdated Show resolved Hide resolved
@benibenj
Copy link
Contributor Author

benibenj commented Sep 5, 2023

Added support for non-tabs. However, the setting is still called 'tabHeight' which might be confusing as it also applies changes when tabs are hidden. Do you suggest using a different name (might make it harder to find for users using tabs) or is it enough to document it in the setting description? @bpasero

@bpasero bpasero self-requested a review September 6, 2023 07:06
bpasero
bpasero requested changes Sep 6, 2023
View reviewed changes
Copy link
Member

@bpasero bpasero left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cool. I am still uncertain about calling this "tab height" given it applies when tabs are disabled. Another idea would be to stay away from using "tab height" in this PR and rename things to "label height" maybe? The setting description can still made fit to be found when people search for "tab height".

src/vs/workbench/browser/parts/editor/tabsTitleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/tabsTitleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/titleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/noTabsTitleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/noTabsTitleControl.ts Outdated Show resolved Hide resolved
bpasero
bpasero requested changes Sep 6, 2023
View reviewed changes
Copy link
Member

@bpasero bpasero left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Almost!

build/lib/stylelint/vscode-known-variables.json Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/titleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/titleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/titleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/tabsTitleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/tabsTitleControl.ts Outdated Show resolved Hide resolved
src/vs/workbench/browser/parts/editor/titleControl.ts Show resolved Hide resolved
@benibenj benibenj merged commit 3e1660e into main Sep 6, 2023
6 checks passed
@benibenj benibenj deleted the benibenj/tabHeight branch September 6, 2023 14:17
@justanotheranonymoususer
Copy link
Contributor

Looks like adding another value with height zero will fix this: #33607
how about that? I'd love such an option.

@github-actions github-actions bot locked and limited conversation to collaborators Oct 21, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@bpasero bpasero bpasero approved these changes

Assignees

@benibenj benibenj

Labels
None yet
Projects
None yet
Milestone
September 2023
Development

Successfully merging this pull request may close these issues.
3 participants
@benibenj @justanotheranonymoususer @bpasero