Auto-formatting in calc

[RustanLeino]

The automatic formatting that dafny-mode performs does not produce nice results in calc statements. In fact, I find the automatic formatting is working against me, and I constantly have to correct what it's doing. I'd love to see this improved.

Repro:

Start with

lemma L() {
  calc {
  }
}

Then, inside the braces that follow the calc statement, type the following lines in order:

A(x);
==
B(x);
C(x);
==  // here is a comment
D(x);
==  { MyFavoriteLemma(x, y); }
E(x);
{ AnotherLemma(x, y); }
F(x);
<
100;

This produces:

lemma L() {
  calc {
    A(x);
    ==
      B(x);
      C(x);
      ==  // here is a comment
        D(x);
        ==  { MyFavoriteLemma(x, y); }
        E(x);
        { AnotherLemma(x, y); }
        F(x);
        <
          100;
  }
}

but I wish it would instead produce:

lemma L() {
  calc {
    A(x);
  ==
    B(x);
    C(x);
  ==  // here is a comment
    D(x);
  ==  { MyFavoriteLemma(x, y); }
    E(x);
    { AnotherLemma(x, y); }
    F(x);
  <
    100;
  }
}

[texastony]

The indenting provided by Boogie Friends,
when working on Dafny,
is a little frustrating.

One day, I hope to have time to push a PR to improve it.
One day...