tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Add diagnostic for pluscal labels inserted by translation #350

Closed hwayne closed 1 week ago

hwayne commented 1 week ago

The PlusCal translator has a -reportLabels flag. When set, it will automatically add missing labels to translations and log that in the output:

pcal.trans Version 1.11 of 31 December 2020
The following label was added:
  Lbl_1 at line 16, column 5
Parsing completed.
Translation completed.

Since it's logged, we might as well tell the user about it! This PR adds an information diagnostic. Demo:

image

image

Questions: