feat: auto-generate header formatter

This commit is contained in:
Sebastian Ullrich 2020-08-21 16:43:55 +02:00
parent fc9b39e48c
commit e5de32c2dd
2 changed files with 2 additions and 2 deletions

View file

@ -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 :=

View file

@ -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;