From d85a41a4d7b8588ba65b68efafe5029b1e0d5483 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Aug 2020 10:55:03 -0700 Subject: [PATCH] chore: reduce number of dependencies @Kha Please try to avoid importing `Lean.Meta`, it is huge, and any change there was forcing a bunch of files to be recompiled since `Parser.Extension` depends on `Parenthesizer` --- src/Lean/PrettyPrinter/Formatter.lean | 2 +- src/Lean/PrettyPrinter/Parenthesizer.lean | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 189b0e4970..371fbff579 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -14,7 +14,7 @@ emitting a token, we already know the text following it and can decide whether o necessary. -/ import Lean.Parser -import Lean.Meta +import Lean.Meta.ReduceEval import Lean.Elab.Quotation namespace Lean diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 862953f547..37487bf03a 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -70,7 +70,9 @@ node). -/ -import Lean.Meta +import Lean.Util.ReplaceExpr +import Lean.Meta.Basic +import Lean.Meta.WHNF import Lean.KeyedDeclsAttribute import Lean.Parser.Basic import Lean.ParserCompiler