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

ichxorya commented 1 month ago

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 commented 1 month ago

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

ichxorya commented 1 month ago

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

joneugster commented 1 month ago

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

leanprover-community / NNG4