indentation of case with dafny-mode in emacs

[robstewart57]

When I write a sequence of case statements, my expectation is that Tab to re-indent dafny code would line up all case occurrences vertically with the same number of space characters from the left of each line. However, each case is lined up with the statements inside of the case above:

method Baz(x:int) returns (y:int)
{
  if {
  case x == 0 =>
    y := 0;
    case 0 < x =>
      y := y + 1;
      case x < 0 =>
        y := y - 1;
  }
}

[cpitclaudel]

Correct. It's tricky to detect these statements; the usual convention is to write them in any of the following forms:

  if {
  case x == 0 => y := 0;
  case 0 < x  => y := y + 1;
  case x < 0  => y := y - 1;
  }

  if {
  case x == 0 => {
    y := 0;
  }
  case 0 < x => {
    y := y + 1;
  }
  case x < 0  => {
    y := y - 1;
  }
  }

  if {
  case x == 0 =>
  { y := 0; }
  case 0 < x =>
  { y := y + 1; }
  case x < 0 =>
  { y := y - 1; }
  }

  if {
  case x == 0 => {
    y := 0;
  } case 0 < x => {
    y := y + 1;
  } case x < 0  => {
    y := y - 1;
  }
  }

The idea being that single-line bodies should either get braces, or be on the same line as the case.