polishSource — Mathlib

Lean4
/-- `polishSource s` is similar to `polishPP s`, but expects the input to be actual source code.
For this reason, `polishSource s` performs more conservative changes:
it only replace all whitespace starting from a linebreak (`\n`) with a single whitespace. -/
def polishSource (s : String) : String × Array Nat :=
  let split := s.split (· == '\n')
  let preWS :=
    split.foldl (init := #[]) fun p q =>
      let txt := q.trimLeft.length
      (p.push (q.length - txt)).push txt
  let preWS := preWS.eraseIdxIfInBounds 0
  let s := (split.map .trimLeft).filter (· != "")
  (" ".intercalate (s.filter (!·.isEmpty)), preWS)
Похожие утверждения