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

UI Suggestions: Hide locked concepts, hot keys and diffing between LHS and RHS #76

Open
ichxorya opened this issue Sep 16, 2024 · 3 comments

Comments

@ichxorya
Copy link

Title. I would like to suggest a few UI improvements to the game.

  • The player should have the right to hide/unhide the locked concepts (tactics, definitions, theorems...) with a button on each topic. That way, they can focus on what they already have.
  • They should also be able to assign hot keys to quickly insert "concepts".
  • For the diffing part, there should also be a hide/unhide button to do the trick. The color scheme should be reasonable, too (though I doubt this is a LSP problem - out of scope for this game).

I would like to introduce these with a PR, but unfortunately I'm still new to Lean and couldn't do much. Hope my idea would help!

@joneugster
Copy link
Collaborator

joneugster commented Sep 17, 2024

Thanks for the suggestions. They are best placed as individual issues at https://github.com/leanprover-community/lean4game/issues

@ichxorya
Copy link
Author

I'm gonna close it for now, thank you.

@ichxorya ichxorya closed this as not planned Won't fix, can't repro, duplicate, stale Sep 17, 2024
@joneugster joneugster reopened this Sep 18, 2024
@joneugster
Copy link
Collaborator

You can keep it open until there are issues on the other repo. I might make them myself once I have time :)

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

No branches or pull requests

2 participants