team-worthwhile/worthwhile — Issue #88: Formatter breaks syntactic correctness and modifies the program iteratively
Author: jspam
Created: 2012-02-21 20:35:46+00:00
State: open
Labels: ui

Trying to format the following program using `Ctrl+Shift+F`:

```
Integer[] funcresults := {1, 2}

_assert ∃ Integer j, 0 ≤ j ∧ j ≤ 1 : funcresults[j] ≥ 0
_assume ∀ Integer k, 0 ≤ k ∧ k ≤ 1 : funcresults[k] ≥ 0
```

yields

```
Integer [] funcresults :={1,
2}

_assert ∃ Integer j,
0 ≤ j ∧ j ≤ 1 : funcresults [ j ] ≥ 0
_assume ∀ Integer k,
0 ≤ k ∧ k ≤ 1 : funcresults [ k ] ≥ 0
```
which is no longer syntactically correct.

After applying the formatter a few times, the program looks like this:

```
Integer [] funcresults :={1,

2 }

_assert ∃ Integer j ,
0 ≤ j ∧ j ≤ 1 : funcresults [ j ] ≥ 0
_assume ∀ Integer k ,
0 ≤ k ∧ k ≤ 1 : funcresults [ k ] ≥ 0
```