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

Reduce clutter in toolbar #3198

Merged
merged 12 commits into from
Jul 15, 2023
Merged

Conversation

FliegendeWurst
Copy link
Member

@FliegendeWurst FliegendeWurst commented Jul 9, 2023

image
View menu:
image

This reduces clutter in the main toolbar by:

  • moving the action history next to the other undo buttons
  • moving the layout controls to a menu (View -> Layout)
  • marking the exploration extension as experimental (as documented)
  • disabling the functionality to reorder toolbars (only ever used by accident)

As a bonus, the bug that extension panels sometimes fail to show up should also be fixed.

@codecov
Copy link

codecov bot commented Jul 9, 2023

Codecov Report

Merging #3198 (85357af) into main (f798501) will not change coverage.
The diff coverage is n/a.

@@            Coverage Diff            @@
##               main    #3198   +/-   ##
=========================================
  Coverage     37.59%   37.59%           
  Complexity    16684    16684           
=========================================
  Files          2043     2043           
  Lines        125713   125713           
  Branches      21106    21106           
=========================================
  Hits          47256    47256           
  Misses        72693    72693           
  Partials       5764     5764           
Impacted Files Coverage Δ
.../key_project/exploration/ExplorationExtension.java 0.00% <ø> (ø)

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

@github-actions
Copy link

github-actions bot commented Jul 9, 2023

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

@wadoon
Copy link
Member

wadoon commented Jul 10, 2023

This reduces clutter in the main toolbar. Other options to consider:

  • moving the layout controls to a menu

Yes the layout toolbar can be moved to a menu.

@FliegendeWurst FliegendeWurst changed the title Move action history button to main toolbar Reduce clutter in toolbar Jul 10, 2023
@FliegendeWurst
Copy link
Member Author

@WolframPfeifer I believe the bug that extension panels sometimes fail to show up is fixed with the latest commit.

@WolframPfeifer
Copy link
Member

@WolframPfeifer I believe the bug that extension panels sometimes fail to show up is fixed with the latest commit.

I tested it by switching to an older branch without proof slicing and then back to this one, and the slicing panel appeared as expected. Thanks!

@FliegendeWurst
Copy link
Member Author

FliegendeWurst commented Jul 14, 2023

Current state:

image

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

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

I have a few final requests (see my suggestions). I would like to have the status line messages harmonized to Layout saved to ... and Layout loaded from ....

Otherwise, I think the PR is fine and really increases usability of KeY.

@FliegendeWurst
Copy link
Member Author

I have integrated all of your suggestions.

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

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

Thanks!

@WolframPfeifer WolframPfeifer added this pull request to the merge queue Jul 15, 2023
Merged via the queue into KeYProject:main with commit c482269 Jul 15, 2023
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants