vscode-tlaplus icon indicating copy to clipboard operation
vscode-tlaplus copied to clipboard

Model checking pane should show location of semantic analysis failures

Open JoshuaRowePhantom opened this issue 3 years ago • 0 comments
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.

JoshuaRowePhantom avatar May 28 '22 15:05 JoshuaRowePhantom