idris-lang
Deprecate old multi-line syntax
Before #1029 we could already use multiline strings with regular quotes ". This feature is now redundant with explicit multiline strings using """ and leads to confusing errors messages such as #3594. It should therefore be deprecated and subsequently removed.
How to
I think this is a nice beginner-friendly issue. The way to implement this can be borrowed from other areas of the compiler with deprecated features such as the old record syntax. The code for it is here. There seem to already be code to detect misuse of multiline strings here but that does not seem to be doing the right thing. So that might be worth investigating. Another area worth exploring is replacing the use of strLitLines by simpleStrLit
That code in the Parser is working for multiline single quoted strings. You can see it in action here:
foo = "dfasd
asdfasd"
returns:
Error: Multi-line string is expected to begin with """.
Main:1:7--1:8
1 | foo = "dfasd
^
The only case that we currently accept multiline strings with single quotes is failing statements (because it hits the string tokens directly):
failing "Undefined
name xxx"
xxx
That parser check doesn't help #3594 because the issue there (an unterminated string) occurs during lexing, and the parser is never engaged. Because the string isn't closed, the lexer goes on parsing normal code as string tokens, and then strings as normal code tokens until it hits the end of the file and sees that it is one " short. And the error ends up on the last " in the file - the beginning of the "string" that it thinks is unterminated.
My fix was to disallow newlines in single quoted strings during lexing, returning an error. This would break those multiline failing statements, which must use """ after the change. I believe multiline failing statements are rare. I'll make the PR and we can discuss another point about whether we want to change the lexer error message there.
