diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index cc77af2920..f541e7cb8e 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -172,6 +172,7 @@ inductive ParserDescr
 | strLit            : ParserDescr
 | charLit           : ParserDescr
 | nameLit           : ParserDescr
+| interpolatedStr   : ParserDescr → ParserDescr -- interpolated string
 | ident             : ParserDescr
 | cat               : Name → Nat → ParserDescr
 | parser            : Name → ParserDescr
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 1010645198..9f2fe349ad 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 /-! Extensible parsing via attributes -/
 
 import Lean.Parser.Basic
+import Lean.Parser.StrInterpolation
 import Lean.KeyedDeclsAttribute
 
 namespace Lean
@@ -214,6 +215,7 @@ partial def compileParserDescr (env : Environment) (categories : ParserCategorie
 | ParserDescr.strLit                              => pure $ strLit
 | ParserDescr.charLit                             => pure $ charLit
 | ParserDescr.nameLit                             => pure $ nameLit
+| ParserDescr.interpolatedStr d                   => interpolatedStr <$> compileParserDescr d
 | ParserDescr.ident                               => pure $ ident
 | ParserDescr.nonReservedSymbol tk includeIdent   => pure $ nonReservedSymbol tk includeIdent
 | ParserDescr.parser constName                    => do
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 81bd8d0cb1..fd2d36e9b9 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -26,23 +26,24 @@ def «precedence» := parser! ":" >> precedenceLit
 def optPrecedence := optional (try «precedence»)
 
 namespace Syntax
-@[builtinSyntaxParser] def paren         := parser! "(" >> many1 syntaxParser >> ")"
-@[builtinSyntaxParser] def cat           := parser! ident >> optPrecedence
-@[builtinSyntaxParser] def atom          := parser! strLit
-@[builtinSyntaxParser] def num           := parser! nonReservedSymbol "num"
-@[builtinSyntaxParser] def str           := parser! nonReservedSymbol "str"
-@[builtinSyntaxParser] def char          := parser! nonReservedSymbol "char"
-@[builtinSyntaxParser] def ident         := parser! nonReservedSymbol "ident"
-@[builtinSyntaxParser] def try           := parser! nonReservedSymbol "try " >> syntaxParser maxPrec
-@[builtinSyntaxParser] def lookahead     := parser! nonReservedSymbol "lookahead " >> syntaxParser maxPrec
-@[builtinSyntaxParser] def sepBy         := parser! nonReservedSymbol "sepBy " >> syntaxParser maxPrec >> syntaxParser maxPrec
-@[builtinSyntaxParser] def sepBy1        := parser! nonReservedSymbol "sepBy1 " >> syntaxParser maxPrec >> syntaxParser maxPrec
-@[builtinSyntaxParser] def notFollowedBy := parser! nonReservedSymbol "notFollowedBy " >> syntaxParser maxPrec
+@[builtinSyntaxParser] def paren           := parser! "(" >> many1 syntaxParser >> ")"
+@[builtinSyntaxParser] def cat             := parser! ident >> optPrecedence
+@[builtinSyntaxParser] def atom            := parser! strLit
+@[builtinSyntaxParser] def num             := parser! nonReservedSymbol "num"
+@[builtinSyntaxParser] def str             := parser! nonReservedSymbol "str"
+@[builtinSyntaxParser] def char            := parser! nonReservedSymbol "char"
+@[builtinSyntaxParser] def ident           := parser! nonReservedSymbol "ident"
+@[builtinSyntaxParser] def interpolatedStr := parser! nonReservedSymbol "interpolatedStr " >> syntaxParser maxPrec
+@[builtinSyntaxParser] def try             := parser! nonReservedSymbol "try " >> syntaxParser maxPrec
+@[builtinSyntaxParser] def lookahead       := parser! nonReservedSymbol "lookahead " >> syntaxParser maxPrec
+@[builtinSyntaxParser] def sepBy           := parser! nonReservedSymbol "sepBy " >> syntaxParser maxPrec >> syntaxParser maxPrec
+@[builtinSyntaxParser] def sepBy1          := parser! nonReservedSymbol "sepBy1 " >> syntaxParser maxPrec >> syntaxParser maxPrec
+@[builtinSyntaxParser] def notFollowedBy   := parser! nonReservedSymbol "notFollowedBy " >> syntaxParser maxPrec
 
-@[builtinSyntaxParser] def optional      := tparser! "?"
-@[builtinSyntaxParser] def many          := tparser! "*"
-@[builtinSyntaxParser] def many1         := tparser! "+"
-@[builtinSyntaxParser] def orelse        := tparser!:2 " <|> " >> syntaxParser 1
+@[builtinSyntaxParser] def optional        := tparser! "?"
+@[builtinSyntaxParser] def many            := tparser! "*"
+@[builtinSyntaxParser] def many1           := tparser! "+"
+@[builtinSyntaxParser] def orelse          := tparser!:2 " <|> " >> syntaxParser 1
 
 end Syntax
 
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 6ab58d9782..4ce2fce075 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -15,7 +15,6 @@ already know the text following it and can decide whether or not whitespace betw
 
 import Lean.CoreM
 import Lean.Parser.Extension
-import Lean.Parser.StrInterpolation
 import Lean.KeyedDeclsAttribute
 import Lean.ParserCompiler.Attribute
 import Lean.PrettyPrinter.Backtrack
diff --git a/src/Lean/PrettyPrinter/Meta.lean b/src/Lean/PrettyPrinter/Meta.lean
index 56aba6cb82..e45a760440 100644
--- a/src/Lean/PrettyPrinter/Meta.lean
+++ b/src/Lean/PrettyPrinter/Meta.lean
@@ -41,6 +41,7 @@ unsafe def interpretParserDescr : ParserDescr → AttrM Parenthesizer
 | ParserDescr.charLit                             => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer
 | ParserDescr.nameLit                             => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer
 | ParserDescr.ident                               => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer
+| ParserDescr.interpolatedStr d                   => interpolatedStr.parenthesizer <$> interpretParserDescr d
 | ParserDescr.nonReservedSymbol tk includeIdent   => pure $ nonReservedSymbol.parenthesizer
 | ParserDescr.parser constName                    => interpretParser (ctx interpretParserDescr) constName
 | ParserDescr.cat catName prec                    => pure $ categoryParser.parenthesizer catName prec
@@ -73,6 +74,7 @@ unsafe def interpretParserDescr : ParserDescr → AttrM Formatter
 | ParserDescr.strLit                              => pure $ withAntiquot.formatter (mkAntiquot.formatter' "strLit" `strLit) strLitNoAntiquot.formatter
 | ParserDescr.charLit                             => pure $ withAntiquot.formatter (mkAntiquot.formatter' "charLit" `charLit) charLitNoAntiquot.formatter
 | ParserDescr.nameLit                             => pure $ withAntiquot.formatter (mkAntiquot.formatter' "nameLit" `nameLit) nameLitNoAntiquot.formatter
+| ParserDescr.interpolatedStr d                   => interpolatedStr.formatter <$> interpretParserDescr d
 | ParserDescr.ident                               => pure $ withAntiquot.formatter (mkAntiquot.formatter' "ident" `ident) identNoAntiquot.formatter
 | ParserDescr.nonReservedSymbol tk includeIdent   => pure $ nonReservedSymbol.formatter tk
 | ParserDescr.parser constName                    => interpretParser (ctx interpretParserDescr) constName
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index fc86b34578..4c143213ca 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -74,7 +74,6 @@ node).
 import Lean.CoreM
 import Lean.KeyedDeclsAttribute
 import Lean.Parser.Extension
-import Lean.Parser.StrInterpolation
 import Lean.ParserCompiler.Attribute
 import Lean.PrettyPrinter.Backtrack