C-s skips over a blank line.

[jasonhemann]

I don't know if this is considered a feature, but it surprised me. If beneath the type to a function you have a line with any whitespace on it, when you C-s on the type, it'll skip that whitespace-only line and jump to the next totally blank one.

module TestCs

foo : Nat -> Bool

Notice the single space on the line right after the type of foo.

[david-christiansen]

Ah, this is due to the indentation check. This is all necessarily heuristic until we get Idris parsing for us.

The present rule is "insert the code just before the first line whose indentation is less than or equal to the indentation of the type signature". The line with extra spaces is being treated as indented. I could make the rule be "insert the code just before the first line whose indentation is less than or equal to the indentation of the signature or, alternately, the first line containing only whitespace". This will mean that blank lines don't work in signatures anymore, but that might be OK.

I'd really like the parser to do this for us. If only I had more time.

[jasonhemann]

Okay, makes sense. I very much understand the mindset of leaving it this way until there's time to implement the Right Solution. But, of course, your call if you feel like doing some kind of a hack-around.

[david-christiansen]

Oh, I think a hack is perfectly fine here! :)