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):

• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/291
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/282
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/258
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/257
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/256
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/255 (related: TLC's -difftrace command)
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/250
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/211
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/164
• [ ] https://github.com/tlaplus/vscode-tlaplus/issues/119 (related: https://github.com/tlaplus/tlaplus/issues/393)
• [ ] Highlight lassos steps in error traces (related: https://github.com/tlaplus/tlaplus/issues/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 https://github.com/tlaplus/vscode-tlaplus/issues/261