tlaplus: Inconsistency in placement of comments as returned by OpDefOrDeclNode.getComment

We are now using OpDefOrDeclNode.getComment to parse annotations in TLA+ declarations, see this PR. While it works well, we have noticed a few inconsistencies in the placement of comments. For instance, in the recursive definitions, a comment has to be placed between RECURSIVE ... and the definition, whereas in the local definitions, a comment has to be placed in front of LOCAL.

Below you can find an example of how annotations should be placed in front of declarations. It would be great, if SANY was using a more consistent scheme for getComment.

-------- MODULE Annotations ----------
EXTENDS Integers

CONSTANT
  \* @type: Int;
  N

VARIABLE
  \* @type: Set(Int);
  set

\* @pure
\* @type: Int => Int;
Inc(n) == n + 1

\* @type: Int => Int;
LOCAL LocalInc(x) == x + 1

A(n) ==
  LET \* @pure
      \* @type: Int => Int;
      Dec(x) == x + 1
  IN
  Dec(n)

RECURSIVE Fact(_)
\* @tailrec
\* @type: Int => Int;
Fact(n) ==
  IF n <= 1 THEN 1 ELSE n * Fact(n - 1)

\* @tailrec
\* @type: Int -> Int;
FactFun[n \in Int] ==
  IF n <= 1 THEN 1 ELSE n * FactFun[n - 1]

======================================