diff --git a/src/Lean.lean b/src/Lean.lean
index 73a7944d92..a840d18df3 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -25,5 +25,3 @@ import Lean.Delaborator
 import Lean.PrettyPrinter
 import Lean.CoreM
 import Lean.InternalExceptionId
--- import only for `[init]` side-effects
-import Lean.PrettyPrinter.Meta
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 3af3c5ea56..f6196e1f4a 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -234,15 +234,14 @@ def annotateCurPos (stx : Syntax) : Delab := do
   liftM x
 
 partial def delabFor : Name → Delab
-  | k => do
+  | Name.anonymous => failure
+  | k              => do
     let env ← getEnv
     (match (delabAttribute.ext.getState env).table.find? k with
      | some delabs => delabs.firstM id >>= annotateCurPos
      | none        => failure) <|>
-    (match k with
-     | Name.str Name.anonymous _ _ => failure
-     | Name.str n              _ _ => delabFor n.getRoot  -- have `app.Option.some` fall back to `app` etc.
-     | _                           => failure)
+      -- have `app.Option.some` fall back to `app` etc.
+      delabFor k.getRoot
 
 def delab : Delab := do
   let k ← getExprKind
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index b2f72d2708..9a5a53a958 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -246,7 +246,7 @@ builtin_initialize
     descr := "explicitly run hooks normally activated by builtin parser attributes",
     add   := fun decl args persistent => do
       if args.hasArgs then throwError "invalid attribute 'runBuiltinParserAttributeHooks', unexpected argument"
-      runParserAttributeHooks `Name.anonymous decl (builtin := true)
+      runParserAttributeHooks Name.anonymous decl (builtin := true)
   }
 
 builtin_initialize
@@ -255,7 +255,7 @@ builtin_initialize
     descr := "explicitly run hooks normally activated by parser attributes",
     add   := fun decl args persistent => do
       if args.hasArgs then throwError "invalid attribute 'runParserAttributeHooks', unexpected argument"
-      runParserAttributeHooks `Name.anonymous decl (builtin := false)
+      runParserAttributeHooks Name.anonymous decl (builtin := false)
   }
 
 private def ParserExtension.addImported (es : Array (Array ParserExtensionOleanEntry)) : ImportM ParserExtensionState := do
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index c389ac025a..51b287ca2c 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -19,11 +19,10 @@ namespace ParserCompiler
 
 structure Context (α : Type) :=
   (varName : Name)
-  (runtimeAttr : KeyedDeclsAttribute α)
+  (categoryAttr : KeyedDeclsAttribute α)
   (combinatorAttr : CombinatorAttribute)
-  (interpretParserDescr : ParserDescr → AttrM α)
 
-def Context.tyName {α} (ctx : Context α) : Name := ctx.runtimeAttr.defn.valueTypeName
+def Context.tyName {α} (ctx : Context α) : Name := ctx.categoryAttr.defn.valueTypeName
 
 -- replace all references of `Parser` with `tyName` as a first approximation
 def preprocessParserBody {α} (ctx : Context α) (e : Expr) : Expr :=
@@ -32,11 +31,14 @@ def preprocessParserBody {α} (ctx : Context α) (e : Expr) : Expr :=
 section
 open Meta
 
--- translate an expression of type `Parser` into one of type `tyName`
-partial def compileParserBody {α} (ctx : Context α) (e : Expr) (force : Bool := false) : MetaM Expr := do
+variables {α} (ctx : Context α) (force : Bool := false) in
+/--
+  Translate an expression of type `Parser` into one of type `tyName`, tagging intermediary constants with
+  `ctx.combinatorAttr`. If `force` is `false`, refuse to do so for imported constants. -/
+partial def compileParserExpr (e : Expr) : MetaM Expr := do
   let e ← whnfCore e
   match e with
-  | e@(Expr.lam _ _ _ _)     => lambdaLetTelescope e fun xs b => compileParserBody ctx b >>= mkLambdaFVars xs
+  | e@(Expr.lam _ _ _ _)     => lambdaLetTelescope e fun xs b => compileParserExpr b >>= mkLambdaFVars xs
   | e@(Expr.fvar _ _)        => pure e
   | _ => do
     let fn := e.getAppFn
@@ -55,11 +57,11 @@ partial def compileParserBody {α} (ctx : Context α) (e : Expr) (force : Bool :
           let arg   := args[i]
           let paramTy ← inferType param
           let resultTy ← forallTelescope paramTy fun _ b => pure b
-          let arg ← if resultTy.isConstOf ctx.tyName then compileParserBody ctx arg else pure arg
+          let arg ← if resultTy.isConstOf ctx.tyName then compileParserExpr arg else pure arg
           p := mkApp p arg
         pure p
     let env ← getEnv
-    match ctx.combinatorAttr.getDeclFor env c with
+    match ctx.combinatorAttr.getDeclFor? env c with
     | some p => mkCall p
     | none   =>
       let c' := c ++ ctx.varName
@@ -71,7 +73,7 @@ partial def compileParserBody {α} (ctx : Context α) (e : Expr) (force : Bool :
           | throwError! "don't know how to generate {ctx.varName} for non-definition '{e}'"
         unless (env.getModuleIdxFor? c).isNone || force do
           throwError! "refusing to generate code for imported parser declaration '{c}'; use `@[runParserAttributeHooks]` on its definition instead."
-        let value ← compileParserBody ctx $ preprocessParserBody ctx value
+        let value ← compileParserExpr $ preprocessParserBody ctx value
         let ty ← forallTelescope cinfo.type fun params _ =>
           params.foldrM (init := mkConst ctx.tyName) fun param ty => do
             let paramTy ← inferType param;
@@ -93,51 +95,65 @@ partial def compileParserBody {α} (ctx : Context α) (e : Expr) (force : Bool :
         -- back to parser combinators
         let some e' ← unfoldDefinition? e
           | throwError! "don't know how to generate {ctx.varName} for non-parser combinator '{e}'"
-        compileParserBody ctx e'
+        compileParserExpr e'
 end
 
 open Core
 
-/-- Compile the given declaration into a `[(builtin)runtimeAttr declName]` -/
-def compileParser {α} (ctx : Context α) (declName : Name) (builtin : Bool) (force := false) : AttrM Unit := do
+/-- Compile the given declaration into a `[(builtin)categoryAttr declName]` -/
+def compileCategoryParser {α} (ctx : Context α) (declName : Name) (builtin : Bool) : AttrM Unit := do
   -- This will also tag the declaration as a `[combinatorParenthesizer declName]` in case the parser is used by other parsers.
   -- Note that simply having `[(builtin)Parenthesizer]` imply `[combinatorParenthesizer]` is not ideal since builtin
   -- attributes are active only in the next stage, while `[combinatorParenthesizer]` is active immediately (since we never
   -- call them at compile time but only reference them).
-  let (Expr.const c' _ _) ← (compileParserBody ctx (mkConst declName) force).run'
+  let (Expr.const c' _ _) ← (compileParserExpr ctx (mkConst declName) (force := false)).run'
     | unreachable!
   -- We assume that for tagged parsers, the kind is equal to the declaration name. This is automatically true for parsers
   -- using `parser!` or `syntax`.
   let kind := declName
-  addAttribute c' (if builtin then ctx.runtimeAttr.defn.builtinName else ctx.runtimeAttr.defn.name) (mkNullNode #[mkIdent kind])
-  -- When called from `interpretParserDescr`, `declName` might not be a tagged parser, so ignore "not a valid syntax kind" failures
-  <|> pure ()
+  addAttribute c' (if builtin then ctx.categoryAttr.defn.builtinName else ctx.categoryAttr.defn.name) (mkNullNode #[mkIdent kind])
 
-unsafe def interpretParser {α} (ctx : Context α) (constName : Name) (force := false) : AttrM α := do
-  let info ← getConstInfo constName
-  let env ← getEnv
-  if info.type.isConstOf `Lean.Parser.TrailingParser || info.type.isConstOf `Lean.Parser.Parser then
-    match ctx.runtimeAttr.getValues env constName with
-    | p::_ => pure p
-    | _    =>
-      compileParser ctx constName (builtin := false) force
-      evalConst α (constName ++ ctx.varName)
-  else
-    let d ← evalConst TrailingParserDescr constName
-    ctx.interpretParserDescr d
+variables {α} (ctx : Context α) in
+def compileEmbeddedParsers : ParserDescr → MetaM Unit
+  | ParserDescr.parser constName                    => discard $ compileParserExpr ctx (mkConst constName) (force := false)
+  | ParserDescr.andthen d₁ d₂                       => compileEmbeddedParsers d₁ *> compileEmbeddedParsers d₂
+  | ParserDescr.orelse d₁ d₂                        => compileEmbeddedParsers d₁ *> compileEmbeddedParsers d₂
+  | ParserDescr.optional d                          => compileEmbeddedParsers d
+  | ParserDescr.lookahead d                         => compileEmbeddedParsers d
+  | ParserDescr.try d                               => compileEmbeddedParsers d
+  | ParserDescr.notFollowedBy d                     => compileEmbeddedParsers d
+  | ParserDescr.many d                              => compileEmbeddedParsers d
+  | ParserDescr.many1 d                             => compileEmbeddedParsers d
+  | ParserDescr.sepBy d₁ d₂                         => compileEmbeddedParsers d₁ *> compileEmbeddedParsers d₂
+  | ParserDescr.sepBy1 d₁ d₂                        => compileEmbeddedParsers d₁ *> compileEmbeddedParsers d₂
+  | ParserDescr.node k prec d                       => compileEmbeddedParsers d
+  | ParserDescr.trailingNode k prec d               => compileEmbeddedParsers d
+  | ParserDescr.interpolatedStr d                   => compileEmbeddedParsers d
+  | ParserDescr.symbol tk                           => pure ()
+  | ParserDescr.numLit                              => pure ()
+  | ParserDescr.strLit                              => pure ()
+  | ParserDescr.charLit                             => pure ()
+  | ParserDescr.nameLit                             => pure ()
+  | ParserDescr.ident                               => pure ()
+  | ParserDescr.nonReservedSymbol tk includeIdent   => pure ()
+  | ParserDescr.noWs                                => pure ()
+  | ParserDescr.cat catName prec                    => pure ()
 
+/-- Precondition: `α` must match `ctx.tyName`. -/
 unsafe def registerParserCompiler {α} (ctx : Context α) : IO Unit := do
   Parser.registerParserAttributeHook {
-    postAdd := fun catName declName builtin => do
-      -- force compilation of parser even if imported, which can be the case with `[runBuiltinParserAttributeHooks]`
-      if builtin then
-        compileParser ctx declName builtin (force := true)
+    postAdd := fun catName constName builtin => do
+      let info ← getConstInfo constName
+      if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then
+        let d ← evalConstCheck ParserDescr `Lean.ParserDescr constName <|>
+          evalConstCheck TrailingParserDescr `Lean.TrailingParserDescr constName
+        compileEmbeddedParsers ctx d $.run'
       else
-        let p ← interpretParser ctx declName (force := true)
-        -- Register `p` without exporting it to the .olean file. It will be re-interpreted and registered
-        -- when the parser is imported.
-        let env ← getEnv
-        setEnv $ ctx.runtimeAttr.ext.modifyState env fun st => { st with table := st.table.insert declName p }
+        if catName.isAnonymous then
+          -- `[runBuiltinParserAttributeHooks]` => force compilation even if imported, do not apply `ctx.categoryAttr`.
+          discard (compileParserExpr ctx (mkConst constName) (force := true)).run'
+        else
+          compileCategoryParser ctx constName builtin
   }
 
 end ParserCompiler
diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean
index bd95801122..d9c05073ed 100644
--- a/src/Lean/ParserCompiler/Attribute.lean
+++ b/src/Lean/ParserCompiler/Attribute.lean
@@ -12,7 +12,7 @@ namespace Lean
 namespace ParserCompiler
 
 structure CombinatorAttribute :=
-  (attr : AttributeImpl)
+  (impl : AttributeImpl)
   (ext  : SimplePersistentEnvExtension (Name × Name) (NameMap Name))
 
 -- TODO(Sebastian): We'll probably want priority support here at some point
@@ -36,18 +36,23 @@ def registerCombinatorAttribute (name : Name) (descr : String)
       | none            => throwError $ "invalid [" ++ name ++ "] argument, expected identifier"
   }
   registerBuiltinAttribute attrImpl
-  pure { attr := attrImpl, ext := ext }
+  pure { impl := attrImpl, ext := ext }
 
 namespace CombinatorAttribute
 
-instance : Inhabited CombinatorAttribute := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
+instance : Inhabited CombinatorAttribute := ⟨{impl := arbitrary _, ext := arbitrary _}⟩
 
-def getDeclFor (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) : Option Name :=
+def getDeclFor? (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) : Option Name :=
   (attr.ext.getState env).find? parserDecl
 
 def setDeclFor (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) (decl : Name) : Environment :=
   attr.ext.addEntry env (parserDecl, decl)
 
+unsafe def runDeclFor {α} (attr : CombinatorAttribute) (parserDecl : Name) : CoreM α := do
+  match attr.getDeclFor? (← getEnv) parserDecl with
+  | some d => evalConst α d
+  | _      => throwError! "no declaration of attribute [{attr.impl.name}] found for '{parserDecl}'"
+
 end CombinatorAttribute
 
 end ParserCompiler
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 0cb03f8c51..56811184a3 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -7,6 +7,7 @@ import Lean.Delaborator
 import Lean.PrettyPrinter.Parenthesizer
 import Lean.PrettyPrinter.Formatter
 import Lean.Parser.Module
+import Lean.ParserCompiler
 
 namespace Lean
 
@@ -64,7 +65,12 @@ builtin_initialize
   }
 
 builtin_initialize
-  registerTraceClass `PrettyPrinter;
+  registerTraceClass `PrettyPrinter
+
+@[builtinInit]
+unsafe def registerParserCompilers : IO Unit := do
+  ParserCompiler.registerParserCompiler ⟨`parenthesizer, parenthesizerAttribute, combinatorParenthesizerAttribute⟩
+  ParserCompiler.registerParserCompiler ⟨`formatter, formatterAttribute, combinatorFormatterAttribute⟩
 
 end PrettyPrinter
 end Lean
diff --git a/src/Lean/PrettyPrinter/Backtrack.lean b/src/Lean/PrettyPrinter/Backtrack.lean
deleted file mode 100644
index 410f6133a9..0000000000
--- a/src/Lean/PrettyPrinter/Backtrack.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-/-
-Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
-import Lean.InternalExceptionId
-
-namespace Lean
-namespace PrettyPrinter
-
-/- Auxiliary internal exception for backtracking the pretty printer.
-   See `orelse.parenthesizer` for example -/
-builtin_initialize backtrackExceptionId : InternalExceptionId ← registerInternalExceptionId `backtrackFormatter
-
-end PrettyPrinter
-end Lean
diff --git a/src/Lean/PrettyPrinter/Basic.lean b/src/Lean/PrettyPrinter/Basic.lean
new file mode 100644
index 0000000000..11ce863f89
--- /dev/null
+++ b/src/Lean/PrettyPrinter/Basic.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+import Lean.InternalExceptionId
+import Lean.KeyedDeclsAttribute
+
+namespace Lean
+namespace PrettyPrinter
+
+/- Auxiliary internal exception for backtracking the pretty printer.
+   See `orelse.parenthesizer` for example -/
+builtin_initialize backtrackExceptionId : InternalExceptionId ← registerInternalExceptionId `backtrackFormatter
+
+unsafe def runForNodeKind {α} (attr : KeyedDeclsAttribute α) (k : SyntaxNodeKind) (interp : ParserDescr → CoreM α) : CoreM α := do
+  match attr.getValues (← getEnv) k with
+  | p::_ => pure p
+  | _ =>
+    -- assume `k` is from a `ParserDescr`, in which case we assume it's also the declaration name
+    let info ← getConstInfo k
+    if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then
+      let d ← evalConst ParserDescr k
+      interp d
+    else
+      throwError! "no declaration of attribute [{attr.defn.name}] found for '{k}'"
+
+end PrettyPrinter
+end Lean
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 6e641d4246..52f4cfca43 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -17,7 +17,7 @@ import Lean.CoreM
 import Lean.Parser.Extension
 import Lean.KeyedDeclsAttribute
 import Lean.ParserCompiler.Attribute
-import Lean.PrettyPrinter.Backtrack
+import Lean.PrettyPrinter.Basic
 
 namespace Lean
 namespace PrettyPrinter
@@ -156,11 +156,15 @@ def group (x : Formatter) : Formatter := do
 @[extern "lean_mk_antiquot_formatter"]
 constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter
 
-def formatterForKind (k : SyntaxNodeKind) : Formatter := do
-  let env ← getEnv
-  let p::_ ← pure $ formatterAttribute.getValues env k
-    | throwError! "no known formatter for kind '{k}'"
-  p
+-- break up big mutual recursion
+@[extern "lean_pretty_printer_formatter_interpret_parser_descr"]
+constant interpretParserDescr' : ParserDescr → CoreM Formatter := arbitrary _
+
+unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do
+  (← liftM $ runForNodeKind formatterAttribute k interpretParserDescr')
+
+@[implementedBy formatterForKindUnsafe]
+constant formatterForKind (k : SyntaxNodeKind) : Formatter := arbitrary _
 
 @[combinatorFormatter Lean.Parser.withAntiquot]
 def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
@@ -396,6 +400,32 @@ def interpolatedStr.formatter (p : Formatter) : Formatter := do
 @[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=
   if c then t else e
 
+@[export lean_pretty_printer_formatter_interpret_parser_descr]
+unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
+  | ParserDescr.andthen d₁ d₂                       => andthen.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.orelse d₁ d₂                        => orelse.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.optional d                          => optional.formatter <$> interpretParserDescr d
+  | ParserDescr.lookahead d                         => lookahead.formatter <$> interpretParserDescr d
+  | ParserDescr.try d                               => try.formatter <$> interpretParserDescr d
+  | ParserDescr.notFollowedBy d                     => notFollowedBy.formatter <$> interpretParserDescr d
+  | ParserDescr.many d                              => many.formatter <$> interpretParserDescr d
+  | ParserDescr.many1 d                             => many1.formatter <$> interpretParserDescr d
+  | ParserDescr.sepBy d₁ d₂                         => sepBy.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.sepBy1 d₁ d₂                        => sepBy1.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.node k prec d                       => node.formatter k <$> interpretParserDescr d
+  | ParserDescr.trailingNode k prec d               => trailingNode.formatter k prec <$> interpretParserDescr d
+  | ParserDescr.symbol tk                           => pure $ symbol.formatter tk
+  | ParserDescr.numLit                              => pure $ withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.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.ident                               => pure $ withAntiquot.formatter (mkAntiquot.formatter' "ident" `ident) identNoAntiquot.formatter
+  | ParserDescr.interpolatedStr d                   => interpolatedStr.formatter <$> interpretParserDescr d
+  | ParserDescr.nonReservedSymbol tk includeIdent   => pure $ nonReservedSymbol.formatter tk
+  | ParserDescr.noWs                                => pure $ checkNoWsBefore.formatter
+  | ParserDescr.parser constName                    => combinatorFormatterAttribute.runDeclFor constName
+  | ParserDescr.cat catName prec                    => pure $ categoryParser.formatter catName
+
 end Formatter
 open Formatter
 
diff --git a/src/Lean/PrettyPrinter/Meta.lean b/src/Lean/PrettyPrinter/Meta.lean
deleted file mode 100644
index cd495e988a..0000000000
--- a/src/Lean/PrettyPrinter/Meta.lean
+++ /dev/null
@@ -1,91 +0,0 @@
-/-
-Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
-
-/-!
-Set up pretty printer compilers for the next stage.
--/
-
-import Lean.PrettyPrinter.Parenthesizer
-import Lean.PrettyPrinter.Formatter
-import Lean.ParserCompiler
-
-namespace Lean
-namespace PrettyPrinter
-
-open Lean.ParserCompiler
-
-namespace Parenthesizer
-
-def ctx (interp) : ParserCompiler.Context Parenthesizer :=
-⟨`parenthesizer, parenthesizerAttribute, combinatorParenthesizerAttribute, interp⟩
-
-unsafe def interpretParserDescr : ParserDescr → AttrM Parenthesizer
-  | ParserDescr.andthen d₁ d₂                       => andthen.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.orelse d₁ d₂                        => orelse.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.optional d                          => optional.parenthesizer <$> interpretParserDescr d
-  | ParserDescr.lookahead d                         => lookahead.parenthesizer <$> interpretParserDescr d
-  | ParserDescr.try d                               => try.parenthesizer <$> interpretParserDescr d
-  | ParserDescr.notFollowedBy d                     => notFollowedBy.parenthesizer <$> interpretParserDescr d
-  | ParserDescr.many d                              => many.parenthesizer <$> interpretParserDescr d
-  | ParserDescr.many1 d                             => many1.parenthesizer <$> interpretParserDescr d
-  | ParserDescr.sepBy d₁ d₂                         => sepBy.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.sepBy1 d₁ d₂                        => sepBy1.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.node k prec d                       => leadingNode.parenthesizer k prec <$> interpretParserDescr d
-  | ParserDescr.trailingNode k prec d               => trailingNode.parenthesizer k prec <$> interpretParserDescr d
-  | ParserDescr.symbol tk                           => pure $ symbol.parenthesizer tk
-  | ParserDescr.numLit                              => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer
-  | ParserDescr.strLit                              => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.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 tk includeIdent
-  | ParserDescr.noWs                                => pure $ checkNoWsBefore.parenthesizer
-  | ParserDescr.parser constName                    => interpretParser (ctx interpretParserDescr) constName
-  | ParserDescr.cat catName prec                    => pure $ categoryParser.parenthesizer catName prec
-
-@[builtinInit] unsafe def regHook : IO Unit :=
-  ParserCompiler.registerParserCompiler (ctx interpretParserDescr)
-
-end Parenthesizer
-
-namespace Formatter
-
-def ctx (interp) : ParserCompiler.Context Formatter :=
-  ⟨`formatter, formatterAttribute, combinatorFormatterAttribute, interp⟩
-
-unsafe def interpretParserDescr : ParserDescr → AttrM Formatter
-  | ParserDescr.andthen d₁ d₂                       => andthen.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.orelse d₁ d₂                        => orelse.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.optional d                          => optional.formatter <$> interpretParserDescr d
-  | ParserDescr.lookahead d                         => lookahead.formatter <$> interpretParserDescr d
-  | ParserDescr.try d                               => try.formatter <$> interpretParserDescr d
-  | ParserDescr.notFollowedBy d                     => notFollowedBy.formatter <$> interpretParserDescr d
-  | ParserDescr.many d                              => many.formatter <$> interpretParserDescr d
-  | ParserDescr.many1 d                             => many1.formatter <$> interpretParserDescr d
-  | ParserDescr.sepBy d₁ d₂                         => sepBy.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.sepBy1 d₁ d₂                        => sepBy1.formatter <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
-  | ParserDescr.node k prec d                       => node.formatter k <$> interpretParserDescr d
-  | ParserDescr.trailingNode k prec d               => trailingNode.formatter k prec <$> interpretParserDescr d
-  | ParserDescr.symbol tk                           => pure $ symbol.formatter tk
-  | ParserDescr.numLit                              => pure $ withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.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.noWs                                => pure $ checkNoWsBefore.formatter
-  | ParserDescr.parser constName                    => interpretParser (ctx interpretParserDescr) constName
-  | ParserDescr.cat catName prec                    => pure $ categoryParser.formatter catName
-
-@[builtinInit] unsafe def regHook : IO Unit :=
-  ParserCompiler.registerParserCompiler (ctx interpretParserDescr)
-
-end Formatter
-
-end PrettyPrinter
-end Lean
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index b279216f0d..e95fe48e9f 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -75,7 +75,7 @@ import Lean.CoreM
 import Lean.KeyedDeclsAttribute
 import Lean.Parser.Extension
 import Lean.ParserCompiler.Attribute
-import Lean.PrettyPrinter.Backtrack
+import Lean.PrettyPrinter.Basic
 
 namespace Lean
 namespace PrettyPrinter
@@ -268,11 +268,15 @@ constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind
 def throwError {α} (msg : MessageData) : ParenthesizerM α :=
   liftCoreM $ Lean.throwError msg
 
-def parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer := do
-  let env ← getEnv
-  let p::_ ← pure $ parenthesizerAttribute.getValues env k
-    | throwError! "no known parenthesizer for kind '{k}'"
-  p
+-- break up big mutual recursion
+@[extern "lean_pretty_printer_parenthesizer_interpret_parser_descr"]
+constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer := arbitrary _
+
+unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
+  (← liftM $ runForNodeKind parenthesizerAttribute k interpretParserDescr')
+
+@[implementedBy parenthesizerForKindUnsafe]
+constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer := arbitrary _
 
 @[combinatorParenthesizer Lean.Parser.withAntiquot]
 def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer :=
@@ -473,6 +477,32 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
 @[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
   if c then t else e
 
+@[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
+unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
+  | ParserDescr.andthen d₁ d₂                       => andthen.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.orelse d₁ d₂                        => orelse.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.optional d                          => optional.parenthesizer <$> interpretParserDescr d
+  | ParserDescr.lookahead d                         => lookahead.parenthesizer <$> interpretParserDescr d
+  | ParserDescr.try d                               => try.parenthesizer <$> interpretParserDescr d
+  | ParserDescr.notFollowedBy d                     => notFollowedBy.parenthesizer <$> interpretParserDescr d
+  | ParserDescr.many d                              => many.parenthesizer <$> interpretParserDescr d
+  | ParserDescr.many1 d                             => many1.parenthesizer <$> interpretParserDescr d
+  | ParserDescr.sepBy d₁ d₂                         => sepBy.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.sepBy1 d₁ d₂                        => sepBy1.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
+  | ParserDescr.node k prec d                       => leadingNode.parenthesizer k prec <$> interpretParserDescr d
+  | ParserDescr.trailingNode k prec d               => trailingNode.parenthesizer k prec <$> interpretParserDescr d
+  | ParserDescr.symbol tk                           => pure $ symbol.parenthesizer tk
+  | ParserDescr.numLit                              => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer
+  | ParserDescr.strLit                              => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.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 tk includeIdent
+  | ParserDescr.noWs                                => pure $ checkNoWsBefore.parenthesizer
+  | ParserDescr.parser constName                    => combinatorParenthesizerAttribute.runDeclFor constName
+  | ParserDescr.cat catName prec                    => pure $ categoryParser.parenthesizer catName prec
+
 end Parenthesizer
 open Parenthesizer
 
diff --git a/tests/lean/ppSyntax.lean b/tests/lean/ppSyntax.lean
new file mode 100644
index 0000000000..76c4d66c46
--- /dev/null
+++ b/tests/lean/ppSyntax.lean
@@ -0,0 +1,9 @@
+import Lean
+
+open Lean
+
+def test (stx : Unhygienic Syntax) : MetaM Unit :=
+  PrettyPrinter.ppTerm stx.run >>= IO.println
+
+-- test imported `ParserDescr`
+#eval test `(s!"hi!")
diff --git a/tests/lean/ppSyntax.lean.expected.out b/tests/lean/ppSyntax.lean.expected.out
new file mode 100644
index 0000000000..7e4cb22b37
--- /dev/null
+++ b/tests/lean/ppSyntax.lean.expected.out
@@ -0,0 +1 @@
+s!"hi!"