leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
199 stars 35 forks source link

Jump to correct tab when introducing new lemmas. #88

Closed TentativeConvert closed 1 year ago

TentativeConvert commented 1 year ago

Example: In NNG > Tutorial World > Level 4, a lemma one_eq_succ_zero becomes newly available. However, this is not visible, as it appears in a hidden tab:

image

It would be helpful if the relevant tab was opened automatically:

image

joneugster commented 1 year ago

Done. If multiple lemmas are added to different tabs in one level, it is undefined which of these tabs is chosen by default. (i.e. just the first one it finds)