This is awesome

[hwayne]

No real issue, just wanted to say how much I appreciate you making this :D

[hwayne]

Not sure how easy this is in VSCode, but one of the things I've configured in my vim extension is coloring in all primed operators. So if you have

/\ foo < bar
/\ foo' \in bar..10

It would also color the foo'. Makes it easier to skim raw TLA+ specs! I'd recommend trying it out if you write a lot of those :)

[alygin]

Thank you so much for the feedback, I really appreciate it! And thanks for the advise on highlighting primed operators. It really makes sense, and should be pretty easy to implement.

[alygin]

It would also color the foo'. Makes it easier to skim raw TLA+ specs!

@hwayne , implemented in v0.7.0 along with many other syntax highlighting improvements.

BTW, any thoughts on proper indentation of TLA+/PlusCal code?

[hwayne]

I don't think there's enough users to have "proper" indentation, but my preference is two spaces. This is because I tend to use a lot of levels. Taking the sample someone provided in favor of four:

ReplaceNode(table, id, new) ==
    LET bs  == table.buckets
        k   == CHOOSE k \in 0..Len(bs): id \in {n.id : n \in bs[k]}
        old == CHOOSE old \in bs[k]: old.id = id
    IN
        [table EXCEPT !.buckets[k] = (bs[k] \ {old}) \cup {new}]

I might rewrite it as

ReplaceNode(table, id, new) ==
  LET 
    bs  == table.buckets
    k == 
      CHOOSE k \in 0..Len(bs):
        id \in {n.id : n \in bs[k]}
    old == 
      CHOOSE old \in bs[k]: 
        old.id = id
  IN
    [table EXCEPT 
      !.buckets[k] = (bs[k] \ {old}) \cup {new}
    ]

That's an extreme example, but it helps when working with /\ and \/ chains.