forall statement visually looks like forall expression

[RustanLeino]

The emacs mode for Dafny visualizes Dafny's forall keyword in two different ways. For forall expressions (that is, universal quantifications), it visualizes the keyword as an ∀. For forall statements it (mostly) visualizes the keyword as itself (forall). Which one to choose is, I believe, determined by a simple syntactic scan of some things that follow the forall keyword. Here is one case where that simple scan makes the wrong determination, which I think can easily be improved.

When the ensures clause happens on the subsequent line, all is good:

      forall x: int | true
        ensures Ǝ y :: x == y
      {
      }

But when the first line contains a :: (even if there's an ensures in between), then the forall turns into a ∀:

      ∀ x: int | true ensures Ǝ y :: x == y {
      }

It would seem that the syntactic scan could look for an ensures. If it finds an ensures before it finds a ::, then the preceding forall is probably a forall statement.