Return to typewriter mode suggestion

[Not-Abram]

I was assigned to play through the game by my professor. When I got to the end of the tutorial world, I left the game in the editor mode, and was confused when I opened up the next world. I believe it would be helpful to add a note in the intro of the first level in the addition world reminding users to switch back to the typewriter mode. My professor also added a change to use consistent language for referencing the typewriter mode.

[joneugster]

Recently we changed it so that Editor mode is persistent after completing a level, as some people preferred to play the entire game in editor mode.

If somebody has an opinion that it should be otherwise, i.e. you start in typewriter in each level, I'm open to have an issue at lean4game talking about that. We need one of the two behaviours, but I don't have a clear opinion what's better for the majority of users :)

[StevenClontz]

My hot take is that the current behavior of persisting (or having the ability to persist) the typewriter/editor preference is a good idea; I can see folks playing the game that want to get into "real" Lean programming sooner than later would prefer the interface closer to actually writing Lean.

I suppose a checkbox could appear in the corner of the editor mode that says "stay in editor mode" - then if that's ticked, you stay in editor mode from level to level; if it's unticked then you revert back to typerwriter mode when changing levels.