vscode-tlaplus
vscode-tlaplus copied to clipboard
Model checking pane should show location of semantic analysis failures
trafficstars
The error trace view says this:
Errors
Unknown operator: `threadStates'.
Semantic errors:
Unknown operator: `threadStates'.
Parsing or semantic analysis failed.
The output window says this:
Semantic processing of module ThreadPool_Correctness_5_Items_3_Threads
Semantic errors:
*** Errors: 1
line 205, col 47 to line 205, col 58 of module ThreadPool
Unknown operator: `threadStates'.
SANY finished.
Starting... (2022-05-28 08:22:57)
Parsing or semantic analysis failed.
Finished in 549ms at (2022-05-28 08:22:57)
As the eye is drawn to the model checking pane, it would be nice to have a hyperlinked copy of the error location there.