Indentation after datatype declaration

[SohumB]

datatype foo = Foo |
  Bar

  lemma hello() {}

dafny-mode seems to not realise that the datatype declaration has completed and wants to indent everything following that extra level. Any ideas?

[cpitclaudel]

I don't have a good fix for this, unfortunately. The issue stems from the datatype line being identified as a function starter. This could be changed, though indenting continuation lines of datatypes properly would be tricky.

I currently handle all of "class" "codatatype" "colemma" "constructor" "copredicate" "datatype" "function" "iterator" "lemma" "method" "newtype" "predicate" "trait" "type" "function method" "predicate method" uniformly; they sould probably be split into two groups (indent vs no indent). If so, then the Bar in your example would not be indented at all (which is arguably better than indenting everything after it :)

Of course, there are ugly workarounds: you can put an empty comment in front of the datatype line. Or you can reindent lemma manually with shift-tab, and then the rest of the file will be fine.