From e5de32c2dda3986b108f42940eefee9e766c8ed9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 21 Aug 2020 16:43:55 +0200
Subject: [PATCH] feat: auto-generate header formatter

---
 src/Lean/Parser/Module.lean | 1 +
 src/Lean/PrettyPrinter.lean | 3 +--
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 0bac3da465..b1f79bae40 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -12,6 +12,7 @@ namespace Parser
 namespace Module
 def «prelude»  := parser! "prelude"
 def «import»   := parser! "import " >> optional "runtime" >> ident
+@[runParserAttributeHooks]
 def header     := parser! optional «prelude» >> many «import»
 
 def updateTokens (c : ParserContext) : ParserContext :=
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index a9727b5a49..af04035737 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -21,8 +21,7 @@ parenthesizeCommand stx >>= formatCommand
 
 def ppModule (stx : Syntax) : CoreM Format := do
 let header := stx.getArg 0;
--- TODO: header formatter is not auto-generated because the parser is not used in any syntax category...
-some f ← pure $ header.reprint | unreachable!; -- format table Lean.Parser.Module.header.formatter header;
+f ← format Lean.Parser.Module.header.formatter header;
 let cmds := stx.getArgs.extract 1 stx.getArgs.size;
 cmds.foldlM (fun f cmd => do
   cmdF ← ppCommand cmd;