tlaplus / vscode-tlaplus

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

Pluscal transpiler errors with a newline before the message are not captured #205

Closed klinvill closed 3 years ago

klinvill commented 3 years ago

I noticed that the parse module command doesn't display any error messages for errors when a symbol is redefined. It looks like this is because errors that appear on a new line after the -- are not picked up by the pluscal parser in tryParseUnrecoverableError(). For example, the spec below results in the following output from the transpiler:

pcal.trans Version 1.11 of 31 December 2020
Parsing completed.

Unrecoverable error:
 --
Process variable x redefined at line 10, column 11.

Example spec:

---- MODULE test_spec ----

CONSTANTS Procs

(* --algorithm test_spec

variables x=0;

process proc \in Procs
variables x=1;
begin
    Incr:
        x := x+1;
end process;

end algorithm; *)

====

Currently the parse module command will fail silently in this case.