From 0d598dcfdf263398d8a68e95bad0d31a40f87b3b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 12 Dec 2022 16:43:13 -0800 Subject: [PATCH] fix: Format.align always prints whitespace --- src/Init/Data/Format/Basic.lean | 6 +++--- src/Init/NotationExtra.lean | 4 ++-- src/Lean/Parser/Term.lean | 2 +- src/Lean/PrettyPrinter/Formatter.lean | 3 +-- tests/lean/1275.lean.expected.out | 6 ++++-- tests/lean/653.lean.expected.out | 2 +- tests/lean/formatTerm.lean.expected.out | 9 ++++----- tests/lean/ppNotationCode.lean.expected.out | 6 ++++-- tests/lean/traceTacticSteps.lean.expected.out | 4 ++-- 9 files changed, 22 insertions(+), 20 deletions(-) diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index e546f40ddb..94d32beb80 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -42,7 +42,7 @@ inductive Format where if the current group does not fit within the allotted column width. -/ | line : Format /-- `align` tells the formatter to pad with spaces to the current indent, - or else add a newline if we are already past the indent. For example: + or else add a newline if we are already at or past the indent. For example: ``` nest 2 <| "." ++ align ++ "a" ++ line ++ "b" ``` @@ -122,7 +122,7 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult | line, flatten, _, _ => if flatten then { space := 1 } else { foundLine := true } | align force, flatten, m, w => if flatten && !force then {} - else if w ≤ m then + else if w < m then { space := (m - w).toNat } else { foundLine := true } @@ -236,7 +236,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou be w (gs' is) else let k ← currColumn - if k ≤ i.indent then + if k < i.indent then pushOutput ("".pushn ' ' (i.indent - k).toNat) endTags i.activeTags be w (gs' is) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 47a1f68db1..ddca513a5b 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -337,9 +337,9 @@ macro_rules section open Lean.Parser.Tactic -syntax cdotTk := patternIgnore("·" <|> ".") +syntax cdotTk := patternIgnore("· " <|> ". ") /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/ -syntax cdotTk ppSpace sepBy1IndentSemicolon(tactic) : tactic +syntax cdotTk sepBy1IndentSemicolon(tactic) : tactic macro_rules | `(tactic| $cdot:cdotTk $tacs*) => `(tactic| {%$cdot $tacs* }%$cdot) end diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 439143cf65..5ec53c71a3 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -191,7 +191,7 @@ The structure type can be specified if not inferable: `{ x := 1, y := 2 : Point }`. -/ @[builtin_term_parser] def structInst := leading_parser - "{" >> withoutPosition (ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with ")) + "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with ")) >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true) >> optEllipsis >> optional (" : " >> termParser)) >> " }" diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 6d6be9abe4..80da39d6ff 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -126,8 +126,7 @@ def pushLine : FormatterM Unit := pushWhitespace Format.line def pushAlign (force : Bool) : FormatterM Unit := - -- don't reset leadWord because .align may introduce zero space - push (.align force) + pushWhitespace (.align force) /-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/ def visitArgs (x : FormatterM Unit) : FormatterM Unit := do diff --git a/tests/lean/1275.lean.expected.out b/tests/lean/1275.lean.expected.out index 68c627bcdb..539c304a7c 100644 --- a/tests/lean/1275.lean.expected.out +++ b/tests/lean/1275.lean.expected.out @@ -3,7 +3,8 @@ fun x => do let scp ← getCurrMacroScope let mainModule ← getMainModule pure - { raw := + { + raw := Syntax.node2 info `term👉__ (Syntax.atom info "👉") x.raw } : (x : TSyntax [`ident, `token._]) → ?m x (TSyntax `term) true @@ -13,7 +14,8 @@ fun x => do let scp ← getCurrMacroScope let mainModule ← getMainModule pure - { raw := + { + raw := Syntax.node2 info `termBarBazBoing (Syntax.atom info "bar") x.raw } : (x : TSyntax [`token.baz, `token.boing]) → ?m x (TSyntax `term) true diff --git a/tests/lean/653.lean.expected.out b/tests/lean/653.lean.expected.out index 3bb31809f7..5c91eb9474 100644 --- a/tests/lean/653.lean.expected.out +++ b/tests/lean/653.lean.expected.out @@ -1,4 +1,4 @@ 653.lean:4:14-4:32: error: function expected at - { } + { } term has type Color ?m ?m ?m diff --git a/tests/lean/formatTerm.lean.expected.out b/tests/lean/formatTerm.lean.expected.out index c4c162919d..c5e4c7c56f 100644 --- a/tests/lean/formatTerm.lean.expected.out +++ b/tests/lean/formatTerm.lean.expected.out @@ -32,23 +32,22 @@ do t✝ else e✝ -def foo✝ := by +def foo✝ := by · skip; skip · skip; skip skip (skip; skip) ( skip; skip try skip; skip - try + try skip skip skip) by - try + try skip skip -by - try +by try skip skip by try skip diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out index 88c998b110..7d37ce5685 100644 --- a/tests/lean/ppNotationCode.lean.expected.out +++ b/tests/lean/ppNotationCode.lean.expected.out @@ -15,7 +15,8 @@ let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure - { raw := + { + raw := Lean.Syntax.node2 info `Lean.Parser.Term.app (Lean.Syntax.ident info (String.toSubstring' "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp) [Lean.Syntax.Preresolved.decl `Nat.add [], Lean.Syntax.Preresolved.namespace `Nat.add]) @@ -63,7 +64,8 @@ let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure - { raw := + { + raw := Lean.Syntax.node2 info `Lean.Parser.Term.app (Lean.Syntax.node3 info `term_+++_ lhs.raw (Lean.Syntax.atom info "+++") rhs.raw) (Lean.Syntax.node info `null (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))) }.raw diff --git a/tests/lean/traceTacticSteps.lean.expected.out b/tests/lean/traceTacticSteps.lean.expected.out index 55be7dd3d9..cd52c46bd9 100644 --- a/tests/lean/traceTacticSteps.lean.expected.out +++ b/tests/lean/traceTacticSteps.lean.expected.out @@ -2,7 +2,7 @@ True [Elab.step.result] True [Elab.step] expected type: True, term - by + by skip trivial [Elab.step.result] ?m @@ -15,7 +15,7 @@ [Elab.step] skip [Elab.step] trivial [Elab.step] (apply And.intro✝) <;> trivial -[Elab.step] focus +[Elab.step] focus apply And.intro✝ with_annotate_state"<;>" skip all_goals trivial