Initial clause is inserted in wrong place for functions with multiline type annotation.

[artemkonenko]

If function has several lines of type annotation then generated initial clause for it should be inserted in the annotation's following line instead the middle of type annotation.

Now it is not.
For example:

addMatrix : Num numType => Vect rows (Vect cols numType)
                           -> Vect rows (Vect cols numType)
                           -> Vect rows (Vect cols numType)

after use ctrl+alt+a:

addMatrix : Num numType => Vect rows (Vect cols numType)
addMatrix xs ys = ?addMatrix_rhs
                           -> Vect rows (Vect cols numType)
                           -> Vect rows (Vect cols numType)

[david-christiansen]

We used to have this problem in idris-mode for Emacs. Unfortunately, solving it correctly requires a parse tree with good location information, but I put in a hack that mostly works, which is to check the indentation of the name that the command is called on, then insert the body before the next line whose indentation is less than or equal to it.

[david-christiansen]

Really, though, we should set up Idris's IDE protocol to tell the editor where it goes. Unfortunately, I don't have time for that right now.

[edwinb]

The vim mode (or rather, the version of the command which updates the file) does this in a differently hacky way, which is simply to put the clause on the next blank line. While this also produces odd results sometimes, at least the most common behaviour is less surprising.

I agree that the right solution is for the protocol to say where to put it. Probably using file location information from the parser.

[archaeron]

thanks for reporting the issue @Dummer

and thanks for giving me two alternatives @david-christiansen and @edwinb
I went for the simpler solution at the moment, i.e. searching for the next empty line and inserting the clause there.

I'm happy to change this behaviour if it causes trouble or the compiler tells me where to put it :)