refactor: remove TokenparserConfig.whitespaceFn again

It was used only in the rarely used `rawFn` parser

src/Lean/Parser/Basic.lean

@@ -104,8 +104,10 @@ def andthen (p q : Parser) : Parser := {
 instance : AndThen Parser where
   andThen a b := andthen a (b ())
 
+def skipFn : TokenParserFn := fun _ s => s
+
 def skip : Parser := {
-  fn   := fun _ s => s
+  fn   := skipFn
   info := epsilonInfo
 }
 
@@ -453,35 +455,6 @@ def mkEmptySubstringAt (s : String) (p : String.Pos) : Substring := {
   str := s, startPos := p, stopPos := p
 }
 
-private def rawAux (startPos : String.Pos) (trailingWs : Bool) : ParserFn := fun c s =>
-  let input   := c.input
-  let stopPos := s.pos
-  let leading := mkEmptySubstringAt input startPos
-  let val     := input.extract startPos stopPos
-  if trailingWs then
-    let s        := c.whitespaceFn c.toTokenParserContext s
-    let stopPos' := s.pos
-    let trailing := { str := input, startPos := stopPos, stopPos := stopPos' : Substring }
-    let atom     := mkAtom (SourceInfo.original leading startPos trailing (startPos + val)) val
-    s.pushSyntax atom
-  else
-    let trailing := mkEmptySubstringAt input stopPos
-    let atom     := mkAtom (SourceInfo.original leading startPos trailing (startPos + val)) val
-    s.pushSyntax atom
-
-/-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`. -/
-def rawFn (p : ParserFn) (trailingWs := false) : ParserFn := fun c s =>
-  let startPos := s.pos
-  let s := p c s
-  if s.hasError then s else rawAux startPos trailingWs c s
-
-def chFn (c : Char) (trailingWs := false) : ParserFn :=
-  rawFn (satisfyFn (fun d => c == d) ("'" ++ toString c ++ "'")) trailingWs
-
-def rawCh (c : Char) (trailingWs := false) : Parser := {
-  fn := chFn c trailingWs
-}
-
 /-- Function to be called directly after parsing a token. When not in an error state, parses following whitespace,
     sets up `SourceInfo`, and pushes result of calling `f` with token substring and info onto stack. -/
 @[specialize]
@@ -503,6 +476,21 @@ def pushToken (f : Substring → SourceInfo → Syntax) (startPos : String.Pos)
 def mkNodeToken (n : SyntaxNodeKind) (startPos : String.Pos) (whitespaceFn : TokenParserFn) : TokenParserFn :=
   pushToken (fun ss info => .mkLit n ss.toString info) startPos whitespaceFn
 
+/-- Match an arbitrary parser and return the consumed String in a `Syntax.atom`. -/
+def rawFn (p : ParserFn) (whitespaceFn : TokenParserFn) : ParserFn := fun c s => Id.run do
+  let startPos := s.pos
+  let s := p c s
+  if s.hasError then
+    return s
+  pushToken (fun ss info => .atom info ss.toString) startPos whitespaceFn c.toTokenParserContext s
+
+def chFn (c : Char) (whitespaceFn : TokenParserFn) : ParserFn :=
+  rawFn (satisfyFn (fun d => c == d) ("'" ++ toString c ++ "'")) whitespaceFn
+
+def rawCh (c : Char) (whitespaceFn : TokenParserFn) : Parser := {
+  fn := chFn c whitespaceFn
+}
+
 private def updateTokenCache (startPos : String.Pos) (s : ParserState) : ParserState :=
   -- do not cache token parsing errors, which are rare and usually fatal and thus not worth an extra field in `TokenCache`
   match s with

src/Lean/Parser/Extension.lean

@@ -449,14 +449,13 @@ def mkParserState (input : String) : ParserState :=
 
 /-- convenience function for testing -/
 def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "<input>")
-  (whitespaceFn := whitespace) (tokenFn := tokenFnCore) : Except String Syntax :=
+    (tokenFn := tokenFnCore) : Except String Syntax :=
   let p := andthenFn whitespace (categoryParserFnImpl catName)
   let c := { mkInputContext input fileName with
     tokens := getTokenTable env
     env
     options := {}
     prec := 0
-    whitespaceFn := whitespaceFn
     tokenFn := tokenFn
   }
   let s := p.run c (mkParserState input)

src/Lean/Parser/Module.lean

@@ -45,7 +45,6 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
     options := {}
     prec := 0
     tokens
-    whitespaceFn := whitespace
     tokenFn := tokenFnCore
   } (mkParserState inputCtx.input)
   let stx := if s.stxStack.isEmpty then .missing else s.stxStack.back
@@ -87,7 +86,6 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext)
     let c := { inputCtx, pmctx with
       prec := 0
       tokens := getTokenTable pmctx.env
-      whitespaceFn := whitespace
       tokenFn := tokenFnCore
     }
     let s := p.run c { cache := initCacheForInput inputCtx.input, pos }

src/Lean/Parser/Term.lean

@@ -11,7 +11,7 @@ namespace Parser
 
 namespace Command
 def commentBody : Parser :=
-{ fn := rawFn (finishCommentBlock (pushMissingOnError := true) 1) (trailingWs := true) }
+{ fn := rawFn (finishCommentBlock (pushMissingOnError := true) 1) (whitespaceFn := whitespace) }
 
 @[combinator_parenthesizer commentBody]
 def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
@@ -387,7 +387,7 @@ existent in the current context, or else fails.
 -- use `rawCh` because ``"`" >> ident`` overlaps with `nameLit`, with the latter being preferred by the tokenizer
 -- note that we cannot use ```"``"``` as a new token either because it would break `precheckedQuot`
 @[builtin_term_parser] def doubleQuotedName := leading_parser
-  "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
+  "`" >> checkNoWsBefore >> rawCh '`' (whitespaceFn := skipFn) >> ident
 
 def letIdBinder :=
   withAntiquot (mkAntiquot "letIdBinder" decl_name% (isPseudoKind := true)) <|

src/Lean/Parser/Types.lean

@@ -293,7 +293,6 @@ instance : Inhabited TokenParserFn where
 
 /-- Parser context updateable in `adaptUncacheableContextFn`. -/
 structure ParserContextCore extends TokenParserContext where
-  whitespaceFn : TokenParserFn
   tokenFn      : TokenParserFn
 
 /-- Opaque parser context updateable using `adaptCacheableContextFn` and `adaptUncacheableContextFn`. -/

src/Lean/PrettyPrinter/Formatter.lean

@@ -325,8 +325,6 @@ def parseToken (s : String) : FormatterM ParserState :=
     options := ← getOptions
     prec := 0
     tokens := (← read).table
-    -- TODO: retriever from `Context` so they can be customized by formatters
-    whitespaceFn := whitespace
     tokenFn := tokenFnCore
   } (Parser.mkParserState s)
 

tests/lean/customWhitespace.lean

@@ -9,7 +9,6 @@ def myWhitespace : TokenParserFn := fun c s =>
 
 def myTerm : Parser where
   fn := adaptUncacheableContextFn (fun ctx => { ctx with
-      whitespaceFn := myWhitespace
       tokenFn := fun c s =>
         -- NOTE: handles identifiers only
         let startPos := s.pos

tests/lean/wsLang.lean

@@ -64,7 +64,6 @@ def wsWhitespace : TokenParserFn :=
 
 def enterProg : Parser where
   fn := adaptUncacheableContextFn (fun ctx => { ctx with
-    whitespaceFn := wsWhitespace
     tokenFn := fun c s =>
       let startPos := s.pos
       let s := satisfyFn (·.isWhitespace) "" c s