tlaplus
Split parsing from PlusCal translation
Automatic module parsing is super useful but gets in the way if a user wants to modify the generated TLA+. In these cases, it would be better to separate parsing and translation into two separate code save actions. The recently introduced checksums and corresponding warnings are a good enough guard rail to remind users of the divergence.
In the example below, I want the algorithm to (temporarily) terminate. When I save the editor, the PlusCal translator reverts my change. Note that the workaround to add an alternative Spec formula is too tedious because it requires modifying the corresponding .cfg, too.
According to a (biased) Twitter poll, this has low priority: https://twitter.com/lemmster/status/1436120376984039444