RFC: Presentation / Demo mode

Proposal

Provide a "Presentation / Demo" mode that would toggle on / off some useful options for using vscode-lean4 when doing talks, demos, or congress presentations.

• User Experience: How does this feature improve the user experience?

  As of today, users have to enable / disable the features one by one, which is cumbersome

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

  Everyone doing presentations / demos with Lean4 / VSCode

• Maintainability: Will this change streamline code maintenance or simplify its structure?

  Should not have a large impact, main change is to store the previous values in some record. Determining the set of options affected could be complex tho.

Community Feedback

This was discussed in person at the Big Proof workshop 3, INI, Cambridge. I'll be happy to move the discussion to Zulip if needed.

I cc @PatrickMassot who originally suggested the presenters to use a different set of options for more feedback on this issue (Patrick please edit this issue as you see fit)

No files, tests, or entry points are named. First define which individually configurable options belong in Presentation / Demo mode and how their previous values are stored and restored. Done means the affected option set and toggle behavior are agreed and implemented for VS Code presentations and demos.