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

Make play button clickable and hide it when irrelevant #6252

Conversation

Procrat
Copy link
Contributor

@Procrat Procrat commented Apr 12, 2023

Pull Request Description

Closes #6177: Clicking the play button should show a spinner icon. The play button should only be visible on execution environments that have one or more execution contexts disabled.

play-button.mp4

Important Notes

There's a bug in the existing code that's exacerbated by this PR: the clickable area for the drop down menu is not directly placed on top of the text. Michael is fixing that in a separate branch (39ce6a2).

Checklist

Please ensure that the following checklist has been satisfied before submitting the PR:

  • The documentation has been updated, if necessary.
  • Screenshots/screencasts have been attached, if there are any visual changes. For interactive or animated visual changes, a screencast is preferred.
  • All code follows the Scala, Java, and Rust style guides. In case you are using a language not listed above, follow the Rust style guide.
  • All code has been tested:
    • Unit tests have been written where possible.
    • If GUI codebase was changed, the GUI was tested when built using ./run ide build.

@Procrat Procrat added the CI: No changelog needed Do not require a changelog entry for this PR. label Apr 12, 2023
@Procrat Procrat linked an issue Apr 13, 2023 that may be closed by this pull request
Copy link
Contributor

@vitvakatu vitvakatu left a comment

Choose a reason for hiding this comment

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

QA: passed

@Procrat Procrat added the CI: Ready to merge This PR is eligible for automatic merge label Apr 13, 2023
@mergify mergify bot merged commit 9db317b into wip/MichaelMauderer/Execution_Context_Dropdown_Menu Apr 13, 2023
@mergify mergify bot deleted the wip/procrat/hide-play-button-6177 branch April 13, 2023 14:06
@farmaazon farmaazon restored the wip/procrat/hide-play-button-6177 branch April 17, 2023 09:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI: No changelog needed Do not require a changelog entry for this PR. CI: Ready to merge This PR is eligible for automatic merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Hiding and showing Play button depending on the current execution mode
3 participants