TLAPM: Show meaningful information in the current proof step view if tlaps is disabled.

[kape1395]

It could either show instructions on how to enable the TLAPS support or should be hidden at all.

[lemmy]

To make it easier for TLA+ beginners, I recommend hiding the proof step view (and the commands) until TLAPS is activated.

[lemmy]

Alternatively, the wording could be adjusted so that beginners understand they likely don't need TLAPS at this stage and can simply ignore the view. The message could also include instructions on how to manually hide the view if desired.

"This view is related to the TLA+ proof system. If you are focused on model checking with TLC or Apalache, which is typical for most TLA+ beginners, you can ignore this view. To hide it, simply right-click on the VSCode action bar and uncheck 'TLA+'. If you later want to use the TLA+ proof system, you can enable it by going to the VSCode settings and checking the appropriate TLA+ integration options."