From 7c8100651e55c39fa38f2abde7f3d637c21d2552 Mon Sep 17 00:00:00 2001
From: Lukas Rytz <lukas.rytz@gmail.com>
Date: Mon, 8 Mar 2021 17:15:22 +0100
Subject: [PATCH] Spec for \" in interpolated strings

---
 spec/01-lexical-syntax.md | 17 ++++++++++-------
 spec/13-syntax-summary.md |  4 +++-
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/spec/01-lexical-syntax.md b/spec/01-lexical-syntax.md
index d0e1771727f9..71d493fe21b6 100644
--- a/spec/01-lexical-syntax.md
+++ b/spec/01-lexical-syntax.md
@@ -503,8 +503,9 @@ not processed, except for Unicode escapes (this is deprecated since 2.13.2).
 #### Interpolated string
 
 ```ebnf
-interpolatedString ::= alphaid ‘"’ {printableChar \ (‘"’ | ‘$’) | escape} ‘"’ 
-                         |  alphaid ‘"""’ {[‘"’] [‘"’] char \ (‘"’ | ‘$’) | escape} {‘"’} ‘"""’
+interpolatedString     ::= alphaid ‘"’ {[‘\’] interpolatedStringPart | ‘\\’ | ‘\"’} ‘"’
+                         | alphaid ‘"""’ {[‘"’] [‘"’] char \ (‘"’ | ‘$’) | escape} {‘"’} ‘"""’
+interpolatedStringPart ::= printableChar \ (‘"’ | ‘$’ | ‘\’) | escape
 escape                 ::= ‘$$’ 
                          | ‘$’ id
                          | ‘$’ BlockExpr
@@ -513,16 +514,18 @@ alphaid                ::= upper idrest
 
 ```
 
-An interpolated string consist of an identifier starting with a letter immediately
+An interpolated string consists of an identifier starting with a letter immediately
 followed by a string literal. There may be no whitespace characters or comments 
-between the leading identifier and the opening quote `”` of the string.
+between the leading identifier and the opening quote `"` of the string.
 The string literal in an interpolated string can be standard (single quote)
 or multi-line (triple quote).
 
 Inside an interpolated string none of the usual escape characters are interpreted
-no matter whether the string literal is normal
-(enclosed in single quotes) or multi-line (enclosed in triple quotes). 
-Instead, there are two new forms of dollar sign escape. 
+no matter whether the string literal is normal (enclosed in single quotes) or
+multi-line (enclosed in triple quotes). Note that the sequence `\"` does not
+close a normal string literal (enclosed in single quotes).
+
+There are two forms of dollar sign escape.
 The most general form encloses an expression in `${` and `}`, i.e. `${expr}`. 
 The expression enclosed in the braces that follow the leading `$` character is of 
 syntactical category BlockExpr. Hence, it can contain multiple statements, 
diff --git a/spec/13-syntax-summary.md b/spec/13-syntax-summary.md
index 837054f5a772..3a7827d728e8 100644
--- a/spec/13-syntax-summary.md
+++ b/spec/13-syntax-summary.md
@@ -61,8 +61,10 @@ stringElement    ::=  charNoDoubleQuoteOrNewline
 multiLineChars   ::=  {[‘"’] [‘"’] charNoDoubleQuote} {‘"’}
 
 interpolatedString 
-                 ::=  alphaid ‘"’ {printableChar \ (‘"’ | ‘\$’) | escape} ‘"’ 
+                 ::=  alphaid ‘"’ {[‘\’] interpolatedStringPart | ‘\\’ | ‘\"’} ‘"’ 
                    |  alphaid ‘"""’ {[‘"’] [‘"’] char \ (‘"’ | ‘\$’) | escape} {‘"’} ‘"""’
+interpolatedStringPart
+                 ::= printableChar \ (‘"’ | ‘$’ | ‘\’) | escape
 escape           ::=  ‘\$\$’ 
                    |  ‘\$’ id 
                    |  ‘\$’ BlockExpr