Split parsing from PlusCal translation

[lemmy]

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.

[lemmy]

According to a (biased) Twitter poll, this has low priority: https://twitter.com/lemmster/status/1436120376984039444