diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index b5abfdd5cb..3309d4c109 100644
--- a/src/Lean/Parser.lean
+++ b/src/Lean/Parser.lean
@@ -17,7 +17,7 @@ namespace Parenthesizer
 
 -- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
 @[export lean_mk_antiquot_parenthesizer]
-def mkAntiquot.parenthesizer (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : PrettyPrinter.Parenthesizer :=
+def mkAntiquot.parenthesizer (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer :=
 Parser.mkAntiquot.parenthesizer name kind anonymous
 
 -- The parenthesizer auto-generated these instances correctly, but tagged them with the wrong kind, since the actual kind
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index ac38fe8e31..6dae5084a6 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -22,6 +22,7 @@ categoryParser `command rbp
   `($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead.
   Multiple command will be put in a `null node, but a single command will not (so that you can directly
   match against a quotation in a command kind's elaborator). -/
+-- TODO: use two separate quotation parsers with parser priorities instead
 @[builtinTermParser] def Term.quot := parser! "`(" >> toggleInsideQuot (termParser <|> many1 commandParser true) >> ")"
 
 namespace Command
@@ -29,6 +30,7 @@ def commentBody : Parser :=
 { fn := rawFn (finishCommentBlock 1) true }
 
 @[combinatorParenthesizer commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+@[combinatorFormatter commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
 def docComment       := parser! "/--" >> commentBody
 def attrArg : Parser := ident <|> strLit <|> numLit
diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean
index ab6dd7643d..eb0cb48452 100644
--- a/src/Lean/Parser/Level.lean
+++ b/src/Lean/Parser/Level.lean
@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Parser.Extension
-import Lean.PrettyPrinter.Parenthesizer  -- necessary for auto-generation
+
+-- necessary for auto-generation
+import Lean.PrettyPrinter.Parenthesizer
+import Lean.PrettyPrinter.Formatter
 
 namespace Lean
 namespace Parser
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 689f993350..4fc7b8abff 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -20,7 +20,8 @@ fun c s =>
 { fn   := underscoreFn,
   info := mkAtomicInfo "ident" }
 
-@[combinatorParenthesizer underscore] def underscore.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+@[combinatorParenthesizer underscore] def underscore.parenthesizer := PrettyPrinter.Parenthesizer.rawIdent.parenthesizer
+@[combinatorFormatter underscore] def underscore.formatter := PrettyPrinter.Formatter.rawIdent.formatter
 
 def ident' : Parser := ident <|> underscore
 
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 9827c86ed7..935c371fce 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -102,8 +102,9 @@ def compileParser {α} (ctx : Context α) (env : Environment) (declName : Name)
 -- 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;
-env.addAttribute c' (if builtin then ctx.runtimeAttr.defn.builtinName else ctx.runtimeAttr.defn.name)
-  (mkNullNode #[mkIdent kind])
+env.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 env
 
 unsafe def interpretParser {α} (ctx : Context α) (constName : Name)
     : StateT Environment IO α :=
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 832ca81258..004c0b980b 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -21,7 +21,7 @@ parenthesizeCommand >=> formatCommand table
 
 def ppModule (table : Parser.TokenTable) (stx : Syntax) : MetaM Format := do
 let header := stx.getArg 0;
-f ← format table (mkConst `Lean.Parser.Module.header) header;
+f ← arbitrary _; --format table (mkConst `Lean.Parser.Module.header) header;
 let cmds := stx.getArgs.extract 1 stx.getArgs.size;
 cmds.foldlM (fun f cmd => do
   cmdF ← ppCommand table cmd;
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 2493156dd4..9357e65e28 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -8,15 +8,13 @@ Authors: Sebastian Ullrich
 The formatter turns a `Syntax` tree into a `Format` object, inserting both mandatory whitespace (to separate adjacent
 tokens) as well as "pretty" optional whitespace.
 
-The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree and the parser that
-produced it, driven by parser-specific handlers registered via an attribute. The traversal is right-to-left so that when
-emitting a token, we already know the text following it and can decide whether or not whitespace between the two is
-necessary.
+The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree, driven by
+parser-specific handlers registered via attributes. The traversal is right-to-left so that when emitting a token, we
+already know the text following it and can decide whether or not whitespace between the two is necessary.
 -/
 
-import Lean.Parser
-import Lean.Meta.ReduceEval
-import Lean.Elab.Quotation
+import Lean.Parser.Extension
+import Lean.KeyedDeclsAttribute
 import Lean.ParserCompiler.Attribute
 
 namespace Lean
@@ -39,7 +37,7 @@ end Formatter
 
 abbrev FormatterM := ReaderT Formatter.Context $ StateT Formatter.State MetaM
 
-abbrev Formatter := Expr → FormatterM Unit
+abbrev Formatter := FormatterM Unit
 
 unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) :=
 KeyedDeclsAttribute.init {
@@ -73,6 +71,7 @@ with `Formatter` in the parameter types."
 namespace Formatter
 
 open Lean.Meta
+open Lean.Parser
 open Lean.Format
 
 instance FormatterM.monadTraverser : Syntax.MonadTraverser FormatterM := ⟨{
@@ -118,12 +117,11 @@ fold (Array.foldl (fun acc f => f ++ acc) Format.nil) x
 def concatArgs (x : FormatterM Unit) : FormatterM Unit :=
 concat (visitArgs x)
 
-set_option class.instance_max_depth 100 -- TODO delete
-
+/-
 /--
   Call an appropriate `[formatter]` depending on the `Parser` `Expr` `p`. After the call, the traverser position
   should be to the left of all nodes produced by `p`, or at the left-most child if there are no other nodes left. -/
-partial def visit : Formatter | p => do
+partial def visit : Formatter := do
 stx ← getCur;
 -- do reductions _except_ for definition unfolding
 p ← liftM $ whnfCore p;
@@ -136,7 +134,7 @@ let p := match c with
 | `charLit => mkConst `Lean.Parser.Term.char
 | `numLit => mkConst `Lean.Parser.Term.num
 | `strLit => mkConst `Lean.Parser.Term.str
-| _ => p;
+:= p;
 env ← liftM getEnv;
 match c >>= (formatterAttribute.ext.getState env).table.find? with
 | some (f::_) => do
@@ -163,38 +161,70 @@ match c >>= (formatterAttribute.ext.getState env).table.find? with
   };
 stack ← getStack;
 trace! `PrettyPrinter.format (" => " ++ (stack.extract sp stack.size).foldl (fun acc f => repr (toString f) ++ " " ++ acc) "")
+-/
 
-open Lean.Parser
+@[combinatorFormatter Lean.Parser.orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter := do
+st ← get;
+-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
+-- them in turn. Uses the syntax traverser non-linearly!
+catch p1 $ fun e => match e with
+  | Exception.other _ "BACKTRACK" => set st *> p2
+  | _                             => throw e
 
-@[builtinFormatter categoryParser]
-def categoryParser.formatter : Formatter | p => do
+-- `mkAntiquot` is quite complex, so we'd rather have its formatter synthesized below the actual parser definition.
+-- Note that there is a mutual recursion
+-- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
+-- anyway.
+--@[extern 7 "lean_mk_antiquot_formatter"]
+constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter :=
+arbitrary _
+
+def formatterForKind (k : SyntaxNodeKind) : Formatter := do
+env ← liftM getEnv;
+p::_ ← pure $ formatterAttribute.getValues env k
+  | throw $ Exception.other Syntax.missing $ "no known formatter for kind '" ++ toString k ++ "'";
+p
+
+@[combinatorFormatter Lean.Parser.withAntiquot]
+def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
+-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
+-- fix the backtracking hack outright.
+orelse.formatter antiP p
+
+@[combinatorFormatter Lean.Parser.categoryParser]
+def categoryParser.formatter (cat : Name) : Formatter := do
 stx ← getCur;
--- visit `(mkCategoryAntiquotParser $(p.getArg! 0) <|> $(mkConst stx.getKind))
-visit (mkAppN (mkConst `Lean.Parser.orelse) #[
-  mkApp (mkConst `Lean.Parser.mkCategoryAntiquotParser) (p.getArg! 0),
-  mkConst stx.getKind])
-
-@[builtinFormatter termParser]
-def termParser.formatter : Formatter | p => do
-stx ← getCur;
--- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot`
-if stx.getKind == nullKind then
-  throw $ Exception.other Syntax.missing "BACKTRACK"
+if stx.getKind == `choice then
+  visitArgs do {
+    stx ← getCur;
+    sp ← getStackSize;
+    stx.getArgs.forM fun stx => formatterForKind stx.getKind;
+    stack ← getStack;
+    when (stack.size > sp && stack.anyRange sp stack.size fun f => pretty f != pretty (stack.get! sp))
+      panic! "Formatter.visit: inequal choice children";
+    -- discard all but one child format
+    setStack $ stack.extract 0 (sp+1)
+  }
 else
-  categoryParser.formatter p
+  withAntiquot.formatter (mkAntiquot.formatter' cat.toString none) (formatterForKind stx.getKind)
 
-@[builtinFormatter withAntiquot]
-def withAntiquot.formatter : Formatter | p =>
--- deoptimize
-visit (mkAppN (mkConst `Lean.Parser.orelse) #[p.getArg! 0, p.getArg! 1])
+@[combinatorFormatter Lean.Parser.categoryParserOfStack]
+def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
+st ← get;
+let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset);
+categoryParser.formatter stx.getId
 
-@[builtinFormatter try]
-def try.formatter : Formatter | p =>
-visit p.appArg!
+@[combinatorFormatter Lean.Parser.try]
+def try.formatter (p : Formatter) : Formatter :=
+p
 
-@[builtinFormatter andthen]
-def andthen.formatter : Formatter | p =>
-visit (p.getArg! 1) *> visit (p.getArg! 0)
+@[combinatorFormatter Lean.Parser.lookahead]
+def lookahead.formatter (p : Formatter) : Formatter :=
+p
+
+@[combinatorFormatter Lean.Parser.andthen]
+def andthen.formatter (p1 p2 : Formatter) : Formatter :=
+p2 *> p1
 
 def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
 stx ← getCur;
@@ -204,20 +234,18 @@ when (k != stx.getKind) $ do {
   throw $ Exception.other Syntax.missing "BACKTRACK"
 }
 
-@[builtinFormatter node]
-def node.formatter : Formatter | p => do
-k ← liftM $ reduceEval $ p.getArg! 0;
+@[combinatorFormatter Lean.Parser.node]
+def node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter := do
 checkKind k;
-concatArgs $ visit p.appArg!
+concatArgs p
 
-@[builtinFormatter trailingNode]
-def trailingNode.formatter : Formatter | p => do
-k ← liftM $ reduceEval $ p.getArg! 0;
+@[combinatorFormatter Lean.Parser.trailingNode]
+def trailingNode.formatter (k : SyntaxNodeKind) (_ : Nat) (p : Formatter) : Formatter := do
 checkKind k;
 concatArgs do
-  visit p.appArg!;
+  p;
   -- leading term, not actually produced by `p`
-  categoryParser.formatter p
+  categoryParser.formatter `foo
 
 def parseToken (s : String) : FormatterM ParserState := do
 ctx ← read;
@@ -244,19 +272,17 @@ else do {
   push tk
 }
 
-@[builtinFormatter symbol]
-def symbol.formatter : Formatter | p => do
-let sym := p.getArg! 0;
-sym ← liftM $ reduceEval sym;
+@[combinatorFormatter symbol]
+def symbol.formatter (sym : String) : Formatter := do
 pushToken sym;
 goLeft
 
-@[builtinFormatter symbolNoWs] def symbolNoWs.formatter := symbol.formatter
-@[builtinFormatter unicodeSymbol] def unicodeSymbol.formatter := symbol.formatter
-@[builtinFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
+@[combinatorFormatter symbolNoWs] def symbolNoWs.formatter := symbol.formatter
+@[combinatorFormatter unicodeSymbol] def unicodeSymbol.formatter := symbol.formatter
+@[combinatorFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
 
-@[builtinFormatter identNoAntiquot]
-def identNoAntiquot.formatter : Formatter | _ => do
+@[combinatorFormatter identNoAntiquot]
+def identNoAntiquot.formatter : Formatter := do
 checkKind identKind;
 stx ← getCur;
 let s := stx.getId.toString;
@@ -268,13 +294,15 @@ let s := if pst.stxStack == #[stx] then s else match stx.getId with
 pushToken s;
 goLeft
 
-@[builtinFormatter rawIdent] def rawIdent.formatter : Formatter | _ => do
+@[combinatorFormatter rawIdent] def rawIdent.formatter : Formatter := do
 checkKind identKind;
 stx ← getCur;
 pushToken stx.getId.toString;
 goLeft
 
-def visitAtom (k : SyntaxNodeKind) : Formatter | p => do
+@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter := rawIdent.formatter
+
+def visitAtom (k : SyntaxNodeKind) : Formatter := do
 stx ← getCur;
 when (k != Name.anonymous) $
   checkKind k;
@@ -283,85 +311,83 @@ Syntax.atom _ val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
 pushToken val;
 goLeft
 
-@[builtinFormatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
-@[builtinFormatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
-@[builtinFormatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
-@[builtinFormatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
-@[builtinFormatter fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
+@[combinatorFormatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
+@[combinatorFormatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
+@[combinatorFormatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
+@[combinatorFormatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
+@[combinatorFormatter fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
 
-@[builtinFormatter many]
-def many.formatter : Formatter | p => do
+@[combinatorFormatter many]
+def many.formatter (p : Formatter) : Formatter := do
 stx ← getCur;
-concatArgs $ stx.getArgs.size.forM $ fun _ => visit (p.getArg! 0)
+concatArgs $ stx.getArgs.size.forM fun _ => p
 
-@[builtinFormatter many1] def many1.formatter : Formatter | p => do
+@[combinatorFormatter many1] def many1.formatter (p : Formatter) : Formatter := do
 stx ← getCur;
 if stx.getKind == nullKind then do
   many.formatter p
 else
   -- can happen with `unboxSingleton = true`
-  visit (p.getArg! 0)
+  p
 
-@[builtinFormatter Parser.optional]
-def optional.formatter : Formatter | p => do
-concatArgs $ visit (p.getArg! 0)
+@[combinatorFormatter Parser.optional]
+def optional.formatter (p : Formatter) : Formatter := do
+concatArgs p
 
-@[builtinFormatter sepBy]
-def sepBy.formatter : Formatter | p => do
+@[combinatorFormatter sepBy]
+def sepBy.formatter (p pSep : Formatter) : Formatter := do
 stx ← getCur;
-concatArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => visit (p.getArg! (i % 2))
+concatArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep
 
-@[builtinFormatter sepBy1] def sepBy1.formatter := sepBy.formatter
+@[combinatorFormatter sepBy1] def sepBy1.formatter := sepBy.formatter
 
-@[builtinFormatter orelse] def orelse.formatter : Formatter | p => do
-st ← get;
--- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
--- them in turn. Uses the syntax traverser non-linearly!
-catch (visit (p.getArg! 0)) $ fun e => match e with
-  | Exception.other _ "BACKTRACK" => set st *> visit (p.getArg! 1)
-  | _                             => throw e
-
-@[builtinFormatter withPosition] def withPosition.formatter : Formatter | p => do
+@[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Position → Formatter) : Formatter := do
 -- call closure with dummy position
-visit $ mkApp (p.getArg! 0) (mkConst `sorryAx [levelZero])
+p ⟨0, 0⟩
 
-@[builtinFormatter setExpected] def setExpected.formatter : Formatter | p => visit (p.getArg! 1)
+@[combinatorFormatter Lean.Parser.setExpected]
+def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :=
+p
 
-@[builtinFormatter checkWsBefore] def checkWsBefore.formatter : Formatter | p => do
+@[combinatorFormatter Lean.Parser.toggleInsideQuot]
+def toggleInsideQuot.formatter (p : Formatter) : Formatter :=
+p
+
+@[combinatorFormatter checkWsBefore] def checkWsBefore.formatter : Formatter := do
 modify fun st => { st with leadWord := "" };
 push " "
 
-@[builtinFormatter checkPrec] def checkPrec.formatter : Formatter | p => pure ()
-@[builtinFormatter checkStackTop] def checkStackTop.formatter : Formatter | p => pure ()
-@[builtinFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter | p => pure ()
-@[builtinFormatter checkTailWs] def checkTailWs.formatter : Formatter | p => pure ()
-@[builtinFormatter checkColGe] def checkColGe.formatter : Formatter | p => pure ()
-@[builtinFormatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter | p => pure ()
+@[combinatorFormatter checkPrec] def checkPrec.formatter : Formatter := pure ()
+@[combinatorFormatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
+@[combinatorFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := pure ()
+@[combinatorFormatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
+@[combinatorFormatter checkColGe] def checkColGe.formatter : Formatter := pure ()
+@[combinatorFormatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
 
-@[builtinFormatter pushNone] def pushNone.formatter : Formatter | p => goLeft
-
-open Lean.Parser.Command
-@[builtinFormatter commentBody] def commentBody.formatter := visitAtom Name.anonymous
+@[combinatorFormatter pushNone] def pushNone.formatter : Formatter := goLeft
 
 -- TODO: delete with old frontend
-@[builtinFormatter quotedSymbol] def quotedSymbol.formatter : Formatter | p => do
+@[combinatorFormatter quotedSymbol] def quotedSymbol.formatter : Formatter := do
 checkKind quotedSymbolKind;
 concatArgs do
   push "`"; goLeft;
-  visitAtom Name.anonymous p;
+  visitAtom Name.anonymous;
   push "`"; goLeft
 
-@[builtinFormatter unquotedSymbol] def unquotedSymbol.formatter := visitAtom Name.anonymous
+@[combinatorFormatter unquotedSymbol] def unquotedSymbol.formatter := visitAtom Name.anonymous
+
+@[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=
+if c then t else e
 
 end Formatter
+open Formatter
 
-def format (table : Parser.TokenTable) (parser : Expr) (stx : Syntax) : MetaM Format := Meta.withAtLeastTransparency Meta.TransparencyMode.default do
-(_, st) ← Formatter.visit parser { table := table } { stxTrav := Syntax.Traverser.fromSyntax stx };
+def format (table : Parser.TokenTable) (formatter : Formatter) (stx : Syntax) : MetaM Format := Meta.withAtLeastTransparency Meta.TransparencyMode.default do
+(_, st) ← formatter { table := table } { stxTrav := Syntax.Traverser.fromSyntax stx };
 pure $ st.stack.get! 0
 
-def formatTerm (table) := format table (mkApp (mkConst `Lean.Parser.termParser) (mkNatLit 0))
-
-def formatCommand (table) := format table (mkApp (mkConst `Lean.Parser.commandParser) (mkNatLit 0))
+def formatTerm (table) := format table $ categoryParser.formatter `term
+def formatCommand (table) := format table $ categoryParser.formatter `command
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `PrettyPrinter.format;
diff --git a/src/Lean/PrettyPrinter/Meta.lean b/src/Lean/PrettyPrinter/Meta.lean
index c3ec6456c6..ef57ffea0b 100644
--- a/src/Lean/PrettyPrinter/Meta.lean
+++ b/src/Lean/PrettyPrinter/Meta.lean
@@ -9,6 +9,7 @@ Set up pretty printer compilers for the next stage.
 -/
 
 import Lean.PrettyPrinter.Parenthesizer
+import Lean.PrettyPrinter.Formatter
 import Lean.ParserCompiler
 
 namespace Lean
@@ -18,8 +19,6 @@ open Lean.ParserCompiler
 
 namespace Parenthesizer
 
---constant interpretParserDescr : ParserDescr → StateT Environment IO Parenthesizer := arbitrary _
-
 def ctx (interp) : ParserCompiler.Context Parenthesizer :=
 ⟨`parenthesizer, parenthesizerAttribute, combinatorParenthesizerAttribute, interp⟩
 
@@ -42,18 +41,7 @@ unsafe def interpretParserDescr : ParserDescr → StateT Environment IO Parenthe
 | ParserDescr.nameLit                             => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer
 | ParserDescr.ident                               => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer
 | ParserDescr.nonReservedSymbol tk includeIdent   => pure $ nonReservedSymbol.parenthesizer
-| ParserDescr.parser constName                    => do
-  env ← get;
-  p ← match combinatorParenthesizerAttribute.getDeclFor env constName with
-  | some p => pure p
-  | none   => do {
-    (Expr.const p _ _, env) ← liftM $ IO.runMeta (compileParserBody (ctx interpretParserDescr) (mkConst constName)) env
-      | unreachable!;
-    set env;
-    pure p
-  };
-  env ← get;
-  liftM $ IO.ofExcept $ env.evalConstCheck Parenthesizer `Lean.PrettyPrinter.Parenthesizer p
+| ParserDescr.parser constName                    => interpretParser (ctx interpretParserDescr) constName
 | ParserDescr.cat catName prec                    => pure $ categoryParser.parenthesizer catName prec
 
 @[init] unsafe def regHook : IO Unit :=
@@ -61,5 +49,37 @@ ParserCompiler.registerParserCompiler (ctx interpretParserDescr)
 
 end Parenthesizer
 
+namespace Formatter
+
+def ctx (interp) : ParserCompiler.Context Formatter :=
+⟨`formatter, formatterAttribute, combinatorFormatterAttribute, interp⟩
+
+unsafe def interpretParserDescr : ParserDescr → StateT Environment IO 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.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.nonReservedSymbol tk includeIdent   => pure $ nonReservedSymbol.formatter tk
+| ParserDescr.parser constName                    => interpretParser (ctx interpretParserDescr) constName
+| ParserDescr.cat catName prec                    => pure $ categoryParser.formatter catName
+
+@[init] unsafe def regHook : IO Unit :=
+ParserCompiler.registerParserCompiler (ctx interpretParserDescr)
+
+end Formatter
+
 end PrettyPrinter
 end Lean