There needs to be some kind of context stack where once you enter a PlusCal block all jlist state changes in the enclosing scope are neutralized until the PlusCal block ends. As-is, they conflict:
---- MODULE Test ----
op ==
/\ 1
/\ 2
(* --algorithm Test
begin assert
/\ 3
/\ 4
end algorithm *)
===
The above will erroneously count the 3 and 4 jlist items as being part of the first jlist. A fix to this will probably be implemented by moving keywords like --algorithm and algorithm into the external scanner to notify it that we're entering & exiting a PlusCal block. The scanner will push & pop the current state onto a stack.
There needs to be some kind of context stack where once you enter a PlusCal block all jlist state changes in the enclosing scope are neutralized until the PlusCal block ends. As-is, they conflict:
The above will erroneously count the
3and4jlist items as being part of the first jlist. A fix to this will probably be implemented by moving keywords like--algorithmandalgorithminto the external scanner to notify it that we're entering & exiting a PlusCal block. The scanner will push & pop the current state onto a stack.