Tabbing a block of TLA+ doesn't preserve indentation of conjunct and disjunct lists

Put(t, d) ==
/\ t \notin waitSet
\* The Producer t must not have initiated its termination.
/\ prod[t] = Cardinality(C)
/\ \/ /\ Len(buffer) < B
      /\ buffer' = Append(buffer, d)
      /\ NotifyOther(t)
   \/ /\ Len(buffer) = B
      /\ Wait(t)
/\ UNCHANGED <<prod,cons>>

vs

Put(t, d) ==
    /\ t \notin waitSet
    \* The Producer t must not have initiated its termination.
    /\ prod[t] = Cardinality(C)
    /\ \/ /\ Len(buffer) < B
        /\ buffer' = Append(buffer, d)
        /\ NotifyOther(t)
    \/ /\ Len(buffer) = B
        /\ Wait(t)
    /\ UNCHANGED <<prod,cons>>

Fortunately in this case, SANY caught it:

Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/BlockingQueuePoisonApple.tla
***Parse Error***

  Precedence conflict between ops \lor in block line 124, col 5 to line 124, col 6 of module BlockingQueuePoisonApple and \land.

Residual stack trace follows:
ExtendableExpr starting at line 124, column 8.
ExtendableExpr starting at line 118, column 5.
Expression starting at line 118, column 5.
Definition starting at line 117, column 1.
Module body starting at line 7, column 1.


Fatal errors while parsing TLA+ spec in file BlockingQueuePoisonApple

tla2sany.semantic.AbortException
*** Abort messages: 1

In module BlockingQueuePoisonApple

Could not parse module BlockingQueuePoisonApple from file BlockingQueuePoisonApple.tla


Starting... (2021-07-10 14:43:26)
Error: Parsing or semantic analysis failed.
Finished in 00s at (2021-07-10 14:43:26)

FWIW: The (Eclipse-based) Toolbox does the right thing when tabbing. :-)

Reproduce the issue in the VS Code extension by tabbing the TLA+ block shown in the report, then inspect the extension's indentation handling for conjunct and disjunct lists. Compare the result with the expected formatting and verify that the resulting specification parses successfully with SANY.