Feature parity with TLA+ Toolbox trace explorer

[lemmy]

The trace exploration feature in VSCode falls short compared to the Toolbox's trace explorer. Considering the widespread use of the VSCode extension, it is important to address the following issues and gaps (chronological order):

• Error-Trace modification/addition annotations broken #291
• Add GUI element to reevaluate ALIAS #282
• Model checking pane should show location of semantic analysis failures #258
• Keyboard accessibility of the error trace window #257
• Cannot click on magnifying glass icon to view long error trace record #256
• Toolbox-like handling of long error trace record differences #255 (related: TLC's -difftrace command)
• Error-trace shows a bag (multiset) like a sequence #250
• Action names from other modules don't get displayed in error trace #211
• Error Trace panel does not show modification of some variables between states #164
• Add support to evaluate trace expression #119 (related: Trace expression evaluation with command-line TLC tlaplus#393)
• Highlight lassos steps in error traces (related: Highlight lassos steps in error traces tlaplus#608)
• Error-trace linking to corresponding action
• ...

To prepare for the eventual replacement of VSCode by the new kid in town, functionality should be implemented in TLC rather than in the Toolbox.

@afonsonf has already modernized the error-view infrastructure in #261