TLAPM parser unexpected identifier **outside** of module definition

[lemmy]

Our TLA+ VSCode extension reports unexpected identifiers outside the module definition. This seems to be an LSP bug, since TLAPS does not report such errors when the same module is parsed on the command line.

SPDX-FileCopyrightText: Copyright (c) 1234 THE TLA+ MEGACORP. All rights reserved.

----- MODULE Foobar -----
=====

markus@avocado [08:53:03] [~/src/TLA/_community/tool-qualification-suite/testgen] [main *]
-> % opam exec -- tlapm --version 
d6365cd

markus@avocado [08:53:07] [~/src/TLA/_community/tool-qualification-suite/testgen] [main *]
-> % opam exec -- tlapm Foobar.tla
(* created new ".tlacache/Foobar.tlaps/Foobar.thy" *)
(* fingerprints written in ".tlacache/Foobar.tlaps/fingerprints" *)
File "./Foobar.tla", line 3, character 1 to line 5, character 5:
[INFO]: All 0 obligation proved.

[lemmy]

/cc @kape1395

[kape1395]

Indeed, the error is reported by the TLAPM LSP, and the TLAPM itself doesn't report the error on the CLI. Will investigate.