syntax highlighting of PlusCal stops and then reappears partially after edits

[chillitom]

Using TLAToolbox-1.5.7-win32.win32.x86_64

I find that after some edits the syntax highlighting of PlusCal stops (a little disconcerting when trying to learn the language) and will slowly appear again in place after further edits.

An example repro would be to take the below spec and to indent the variables section with a tab. The highlighting will stop, then make further edits e.g. add a new line, part of the highlighting will return but not all.

-------------------------------- MODULE wire --------------------------------

EXTENDS Integers

(*--algorithm wire

variables
    people = {"alice", "bob"},
    acc = [p \in people |-> 5];

define
    NoOverdrafts == \A p \in people: acc[p] >= 0
    EventuallyConsistent == <>[](acc["alice"] + acc["bob"] = 10)
end define;

process Wire \in 1..2
    variables
        sender = "alice",
        receiver = "bob",
        amount \in 1..acc[sender];
        

begin
    CheckAndWithdraw:
        if amount <= acc[sender] then
            acc[sender] := acc[sender] - amount;
            
            Deposit:
                acc[receiver] := acc[receiver] + amount;
        end if;

end process;

end algorithm;
*)
\* BEGIN TRANSLATION
VARIABLES people, acc, pc

(* define statement *)
NoOverdrafts == \A p \in people: acc[p] >= 0
EventuallyConsistent == <>[](acc["alice"] + acc["bob"] = 10)

VARIABLES sender, receiver, amount

vars == << people, acc, pc, sender, receiver, amount >>

ProcSet == (1..2)

Init == (* Global variables *)
        /\ people = {"alice", "bob"}
        /\ acc = [p \in people |-> 5]
        (* Process Wire *)
        /\ sender = [self \in 1..2 |-> "alice"]
        /\ receiver = [self \in 1..2 |-> "bob"]
        /\ amount \in [1..2 -> 1..acc[sender[CHOOSE self \in  1..2 : TRUE]]]
        /\ pc = [self \in ProcSet |-> "CheckAndWithdraw"]

CheckAndWithdraw(self) == /\ pc[self] = "CheckAndWithdraw"
                          /\ IF amount[self] <= acc[sender[self]]
                                THEN /\ acc' = [acc EXCEPT ![sender[self]] = acc[sender[self]] - amount[self]]
                                     /\ pc' = [pc EXCEPT ![self] = "Deposit"]
                                ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
                                     /\ acc' = acc
                          /\ UNCHANGED << people, sender, receiver, amount >>

Deposit(self) == /\ pc[self] = "Deposit"
                 /\ acc' = [acc EXCEPT ![receiver[self]] = acc[receiver[self]] + amount[self]]
                 /\ pc' = [pc EXCEPT ![self] = "Done"]
                 /\ UNCHANGED << people, sender, receiver, amount >>

Wire(self) == CheckAndWithdraw(self) \/ Deposit(self)

Next == (\E self \in 1..2: Wire(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION


=============================================================================
\* Modification History
\* Last modified Sat Dec 08 19:51:36 GMT 2018 by Tom
\* Created Sat Dec 08 17:58:05 GMT 2018 by Tom

[lemmy]

Possibly related to #224

[vanyarock01]

Hi, the problem also reproduces on version 1.5.3 on Ubuntu 18.04.

[lemmy]

@vanyarock01 1.5.3 is quite old. Is there a reason why you're still on it?

[vanyarock01]

Not really. I will try to upgrade to the latest version and reproduce the problem.