From 093f0553e707ba4ae3b8440f3ed591c052869eee Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 4 Aug 2020 17:02:36 +0200 Subject: [PATCH] chore: add formatter module docstring --- src/Lean/PrettyPrinter/Formatter.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 60f2d7c0e6..8b07988d02 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -4,6 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. 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. +-/ import Lean.Parser import Lean.Meta import Lean.Elab.Quotation