Skip to content

Commit d17a6d8

Browse files
committed
tlaplus/tlaplus#1173 and tlaplus/tlaplus#1174 introduce two new warnings. These warnings are not recognized by our VSCode extension.
[Feature] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 5e6cd8b commit d17a6d8

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/parsers/tlcCodes.ts

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -234,6 +234,8 @@ export const TLC_LIVE_STATE_PREDICATE_NON_BOOL = registerCode(2250, TlcCodeType.
234234
export const TLC_LIVE_CANNOT_EVAL_FORMULA = registerCode(2251, TlcCodeType.Error);
235235
export const TLC_LIVE_ENCOUNTERED_NONBOOL_PREDICATE = registerCode(2252, TlcCodeType.Error);
236236
export const TLC_LIVE_FORMULA_TAUTOLOGY = registerCode(2253, TlcCodeType.Error);
237+
export const TLC_LIVE_FORMULA_STATE_LEVEL = registerCode(2255, TlcCodeType.Warning);
238+
export const TLC_CONFIG_NO_SPEC_BUT_PROPERTY = registerCode(2257, TlcCodeType.Warning);
237239

238240
export const TLC_EXPECTED_VALUE = registerCode(2215, TlcCodeType.Error);
239241
export const TLC_EXPECTED_EXPRESSION = registerCode(2246, TlcCodeType.Error);

0 commit comments

Comments
 (0)