Lsp formatting

src/Init/Data/Format/Basic.lean

@@ -57,10 +57,16 @@ inductive Format where
   | nil                 : Format
   /--
   A position where a newline may be inserted if the current group does not fit within the allotted
-  column width.
+  column width. When the surrounding group is flattened, `line` becomes a space.
   -/
   | line                : Format
   /--
+  An unconditional newline that indents to the current level.
+  Unlike `line`, `hardLine` always produces a newline and prevents the surrounding group
+  from being flattened.
+  -/
+  | hardLine            : Format
+  /--
   `align` tells the formatter to pad with spaces to the current indentation level, or else add a
   newline if we are already at or past the indent.
 
@@ -80,7 +86,8 @@ inductive Format where
   /--
   A node containing a plain string.
 
-  If the string contains newlines, the formatter emits them and then indents to the current level.
+  If the string contains newlines, the formatter emits them at column 0.
+  Use `Format.line` or `Format.nest` to control indentation of line breaks.
   -/
   | text                : String → Format
   /--
@@ -112,6 +119,7 @@ namespace Format
 def isEmpty : Format → Bool
   | nil          => true
   | line         => false
+  | hardLine     => false
   | align _      => true
   | text msg     => msg == ""
   | nest _ f     => f.isEmpty
@@ -162,16 +170,17 @@ private structure SpaceResult where
 private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
   | nil,          _,       _, _ => {}
   | line,         flatten, _, _ => if flatten then { space := 1 } else { foundLine := true }
+  | hardLine,     flatten, _, _ => { foundLine := true, foundFlattenedHardLine := flatten }
   | align force,  flatten, m, w =>
     if flatten && !force then {}
     else if w < m then
       { space := (m - w).toNat }
     else
       { foundLine := true }
-  | text s,       flatten, _, _ =>
+  | text s,       _, _, _ =>
     let p := String.Internal.posOf s '\n'
     let off := String.Internal.offsetOfPos s p
-    { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, space := off }
+    { foundLine := p != s.rawEndPos, space := off }
   | append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m)
   | nest n f,     flatten, m, w => spaceUptoLine f flatten (m - n) w
   | group f _,    _,       m, w => spaceUptoLine f true m w
@@ -271,14 +280,19 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         be w (gs' is)
       else
         pushOutput (String.Internal.extract s {} p)
-        pushNewline i.indent.toNat
+        pushNewline 0
         let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::is
-        -- after a hard line break, re-evaluate whether to flatten the remaining group
-        -- note that we shouldn't start flattening after a hard break outside a group
         if g.fla == .disallow then
           be w (gs' is)
         else
           pushGroup g.flb is gs w >>= be w
+    | hardLine =>
+      pushNewline i.indent.toNat
+      endTags i.activeTags
+      if g.fla == .disallow then
+        be w (gs' is)
+      else
+        pushGroup g.flb is gs w >>= be w
     | line =>
       match g.flb with
       | FlattenBehavior.allOrNone =>

src/Lean/Data/Format.lean

@@ -47,7 +47,7 @@ open Std
 export Std
   (Format ToFormat Format.nest Format.nil Format.joinSep Format.line
    Format.sbracket Format.bracket Format.group Format.tag Format.pretty
-   Format.fill Format.paren Format.join Format.align)
+   Format.fill Format.paren Format.join Format.align Format.hardLine)
 export ToFormat (format)
 
 instance : ToFormat Name where

src/Lean/Data/Lsp/Capabilities.lean

@@ -136,6 +136,8 @@ structure ServerCapabilities where
   inlayHintProvider?        : Option InlayHintOptions        := none
   signatureHelpProvider?    : Option SignatureHelpOptions    := none
   colorProvider?            : Option DocumentColorOptions    := none
+  documentFormattingProvider : Bool                          := false
+  documentRangeFormattingProvider : Bool                     := false
   experimental?             : Option LeanServerCapabilities  := none
   deriving ToJson, FromJson
 

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -725,5 +725,21 @@ structure ColorInformation where
 structure DocumentColorOptions extends WorkDoneProgressOptions where
   deriving FromJson, ToJson
 
+structure FormattingOptions where
+  tabSize : Nat
+  insertSpaces : Bool
+  deriving FromJson, ToJson
+
+structure DocumentFormattingParams where
+  textDocument : TextDocumentIdentifier
+  options : FormattingOptions
+  deriving FromJson, ToJson
+
+structure DocumentRangeFormattingParams where
+  textDocument : TextDocumentIdentifier
+  range : Range
+  options : FormattingOptions
+  deriving FromJson, ToJson
+
 end Lsp
 end Lean

src/Lean/Parser/Extra.lean

@@ -217,7 +217,7 @@ def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : F
     for i in (List.range stx.getArgs.size).reverse do
       if i % 2 == 0 then p else pSep <|>
         -- If the final separator is a newline, skip it.
-        ((if i == stx.getArgs.size - 1 then pure () else pushWhitespace "\n") *> goLeft)
+        ((if i == stx.getArgs.size - 1 then pure () else pushWhitespace Format.hardLine) *> goLeft)
   -- If there is any newline separator, then we add an `align` at the start
   -- so that `withPosition` will pick up the right column.
   if hasNewlineSep then
@@ -286,7 +286,7 @@ open PrettyPrinter Parser
 
 @[combinator_formatter ppHardSpace, expose] def ppHardSpace.formatter : Formatter := Formatter.pushWhitespace " "
 @[combinator_formatter ppSpace, expose] def ppSpace.formatter : Formatter := Formatter.pushLine
-@[combinator_formatter ppLine, expose] def ppLine.formatter : Formatter := Formatter.pushWhitespace "\n"
+@[combinator_formatter ppLine, expose] def ppLine.formatter : Formatter := Formatter.pushWhitespace Format.hardLine
 @[combinator_formatter ppRealFill, expose] def ppRealFill.formatter (p : Formatter) : Formatter := Formatter.fill p
 @[combinator_formatter ppRealGroup, expose] def ppRealGroup.formatter (p : Formatter) : Formatter := Formatter.group p
 @[combinator_formatter ppIndent, expose] def ppIndent.formatter (p : Formatter) : Formatter := Formatter.indent p

src/Lean/Parser/Term.lean

@@ -859,6 +859,37 @@ def argument       :=
 -- argument precedence is `arg` (i.e. does not accept `lead` precedence)
 @[builtin_term_parser] def app := trailing_parser:leadPrec:maxPrec many1 argument
 
+open Lean.PrettyPrinter.Formatter in
+/--
+Custom formatter for function application that uses allOrNone grouping
+when named arguments are present. This formats named arguments in a
+record-like style (all on one line, or each on its own line) rather
+than greedy line-filling.
+-/
+@[builtin_formatter Lean.Parser.Term.app]
+def appFormatter : PrettyPrinter.Formatter := do
+  checkKind ``app
+  let stx ← Syntax.MonadTraverser.getCur
+  let argsNode := stx.getArg 1
+  let hasNamedArg := argsNode.getArgs.any fun arg =>
+    arg.getKind == ``namedArgument
+  let fmtArgs : PrettyPrinter.Formatter := do
+    let stx ← Syntax.MonadTraverser.getCur
+    visitArgs <| stx.getArgs.size.forM fun _ _ => do
+      let cur ← Syntax.MonadTraverser.getCur
+      let k := cur.getKind
+      if k == ``namedArgument || k == ``ellipsis then
+        formatterForKind k
+      else
+        categoryParser.formatter `term
+      checkWsBefore.formatter
+  visitArgs do
+    if hasNamedArg then
+      Lean.PrettyPrinter.Formatter.group fmtArgs
+    else
+      fmtArgs
+    categoryParser.formatter `term
+
 /--
 The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
 More precisely,

src/Lean/PrettyPrinter/Formatter.lean

@@ -371,12 +371,12 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit
       let preNL := Substring.Raw.contains { ss with stopPos := ss'.startPos } '\n'
       let postNL := Substring.Raw.contains { ss with startPos := ss'.stopPos } '\n'
       if postNL then
-        pushWhitespace "\n"
+        pushWhitespace Format.hardLine
       else if !(← get).leadWord.isEmpty then
         pushLine
       push ss'.toString
       if preNL then
-        pushWhitespace "\n"
+        pushWhitespace Format.hardLine
       else
         pushLine
 
@@ -409,11 +409,9 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit
     -- already separated => use `tk` as is
     if st.leadWord == "" then
       push tk.trimAsciiEnd.copy
-    else if tk.endsWith " " then
+    else
       pushLine
       push tk.trimAsciiEnd.copy
-    else
-      push tk -- preserve special whitespace for tokens like ":=\n"
     modify fun st => { st with leadWord := if tk.trimAsciiStart == tk.toSlice then tk else "", leadWordIdent := ident }
 
   if let SourceInfo.original ss _ _ _ := info then
@@ -426,12 +424,12 @@ def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit
       -- with the actual token, so dedent
       indent (indent := some (-Std.Format.getIndent (← getOptions))) do
         if postNL then
-          pushWhitespace "\n"
+          pushWhitespace Format.hardLine
         else
           pushLine
         pushWhitespace ss'.toString
         if preNL then
-          pushWhitespace "\n"
+          pushWhitespace Format.hardLine
         else
           -- It is conceivable that the start of comment syntax could be misinterpreted as part of a token,
           -- so add the beginning of it as the leadWord.

src/Lean/PrettyPrinter/Source.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Willem Vanhulle
+-/
+module
+
+prelude
+public import Lean.PrettyPrinter
+import Lean.Elab.Import
+import Lean.Elab.Command
+
+namespace Lean.PrettyPrinter
+
+private def isCommentOrBlankLine (line : String) : Bool :=
+  let trimmed := line.trimAsciiStart
+  trimmed.isEmpty || trimmed.startsWith "--"
+
+/-- Strip trailing lines that are pure comments or blank from ppCommand output.
+The formatter's `pushToken` preserves trailing `SourceInfo` comments at incorrect
+indentation (nested under the last expression). The gap extraction re-includes them
+at their correct original indentation.
+Scans backward from the end so only trailing lines are inspected. -/
+public def trimTrailingCommentLines (s : String) : String :=
+  let lines := s.split '\n' |>.toStringList
+  let kept := lines.reverse.dropWhile isCommentOrBlankLine |>.reverse
+  "\n".intercalate kept
+
+/-- Collapse runs of 3+ consecutive newlines down to 2 (at most one blank line).
+Folds over characters, tracking consecutive newline count. -/
+public def collapseBlankLines (s : String) : String :=
+  let (acc, _) := s.foldl (fun (acc, nlCount) c =>
+    if c == '\n' then
+      if nlCount < 2 then (acc.push '\n', nlCount + 1)
+      else (acc, nlCount)
+    else
+      (acc.push c, 0)) ("", 0)
+  acc
+
+/-- Parse all top-level commands from an input context. -/
+private partial def parseCommands (inputCtx : Parser.InputContext) (pmctx : Parser.ParserModuleContext)
+    (parserState : Parser.ModuleParserState) : Array Syntax :=
+  go parserState {} #[]
+where
+  go (mps : Parser.ModuleParserState) (msgs : MessageLog) (acc : Array Syntax) : Array Syntax :=
+    let (stx, mps', msgs') := Parser.parseCommand inputCtx pmctx mps msgs
+    if Parser.isTerminalCommand stx then acc
+    else go mps' msgs' (acc.push stx)
+
+/-- Clean an inter-command gap: collapse excessive blank lines and strip trailing
+non-newline whitespace (original indentation before the next command, which `ppCommand`
+will re-emit at column 0). -/
+public def cleanGap (s : String) : String :=
+  let s := collapseBlankLines s
+  -- Strip trailing spaces/tabs (original indentation) since ppCommand starts at column 0
+  match s.revFind? '\n' with
+  | some pos => String.Pos.Raw.extract s {} (String.Pos.Raw.next s pos.offset)
+  | none     => if s.any (!·.isWhitespace) then s else ""
+
+/-- Extract the inter-command gap from original source and clean it. -/
+private def interCommandGap (contents : String) (prevTailPos : Option String.Pos.Raw)
+    (curStartPos : Option String.Pos.Raw) : String :=
+  match prevTailPos, curStartPos with
+  | some prevEnd, some curStart => cleanGap (String.Pos.Raw.extract contents prevEnd curStart)
+  | none, some curStart       => cleanGap (String.Pos.Raw.extract contents {} curStart)
+  | _, none                     => "\n"
+
+/-- Extract the header text from original source, trimming trailing whitespace. -/
+public def extractHeader (contents : String) (headerStx : Syntax) : String :=
+  let raw := match headerStx.getPos?, headerStx.getTailPos? with
+    | some s, some e => String.Pos.Raw.extract contents s e
+    | _, _           => headerStx.reprint.getD ""
+  raw.trimAsciiEnd.copy
+
+/-- Format the result of `ppCommand`, trimming trailing whitespace and comment lines. -/
+public def cleanCommandOutput (fmtResult : Except Exception Format) (stx : Syntax) : String :=
+  match fmtResult with
+  | .ok fmt  => trimTrailingCommentLines fmt.pretty.trimAsciiEnd.copy
+  | .error _ => trimTrailingCommentLines (stx.reprint.getD "").trimAsciiEnd.copy
+
+/-- Emit a command's original source verbatim, trimming trailing whitespace. -/
+public def verbatimCommand (contents : String) (stx : Syntax) : String :=
+  let raw := match stx.getPos?, stx.getTailPos? with
+    | some s, some e => String.Pos.Raw.extract contents s e
+    | _, _           => stx.reprint.getD ""
+  raw.trimAsciiEnd.copy
+
+/-- Format a sequence of commands. Emits the header verbatim, cleans inter-command gaps,
+and calls `formatCmd` for each command. This is the shared core used by both `ppSource`
+and the LSP formatter. -/
+public def formatCommands [Monad m] (source : String) (headerStx : Syntax)
+    (cmdStxs : Array Syntax) (formatCmd : Syntax → m String) : m String := do
+  let mut result := extractHeader source headerStx
+  let mut prevTailPos := headerStx.getTailPos?
+  for stx in cmdStxs do
+    result := result ++ interCommandGap source prevTailPos stx.getPos?
+    result := result ++ (← formatCmd stx)
+    prevTailPos := stx.getTailPos?
+  if !result.isEmpty && !result.endsWith "\n" then
+    result := result ++ "\n"
+  return result
+
+/-- Pretty-print a Lean source file. Parses the header and commands,
+then pretty-prints each command via `ppCommand`. Only requires parsing,
+not elaboration. Returns the formatted source text. -/
+public def ppSource (contents : String) (fileName : String) (opts : Options := {}) : IO String := do
+  let inputCtx := Parser.mkInputContext contents fileName
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, _) ← Elab.processHeader header opts messages inputCtx (trustLevel := 1024)
+  let pmctx : Parser.ParserModuleContext := { env, options := opts }
+  let cmdStxs := parseCommands inputCtx pmctx parserState
+  let cmdState := Elab.Command.mkState env {} opts
+  let fileMap := FileMap.ofString contents
+  formatCommands contents header.raw cmdStxs fun stx => do
+    let cmdCtx : Elab.Command.Context := {
+      cmdPos := stx.getPos?.getD 0
+      fileName, fileMap
+      snap? := none, cancelTk? := none
+    }
+    let fmtResult ← (Elab.Command.liftCoreM (ppCommand ⟨stx⟩) |>.run cmdCtx |>.run' cmdState).toBaseIO
+    return cleanCommandOutput fmtResult stx
+
+end Lean.PrettyPrinter

src/Lean/Server/FileSource.lean

@@ -113,6 +113,12 @@ instance : FileSource SignatureHelpParams where
 instance : FileSource DocumentColorParams where
   fileSource p := fileSource p.textDocument
 
+instance : FileSource DocumentFormattingParams where
+  fileSource? p := fileSource? p.textDocument
+
+instance : FileSource DocumentRangeFormattingParams where
+  fileSource p := fileSource p.textDocument
+
 /--
 Yields the file source of `item` by attempting to obtain `mod : Name` from `item.data?`. \
 Panics if `item.data?` is not present or does not contain a `mod` field and the first element of a