chore: rename String.endPos -> String.rawEndPos (#10853)

This PR renames `String.endPos` to `String.rawEndPos`, as in a future
release the name `String.endPos` will be taken by the function that is
currently called `String.endValidPos`.

Author: TwoFX

script/Modulize.lean

@@ -57,19 +57,19 @@ def main (args : List String) : IO Unit := do
         sec := "\n\n" ++ sec
       if insertPos?.isNone then
         sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
+      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
 
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
       let prfx := if doMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
+      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
 
     -- insert `module` header
     let mut initText := text.extract 0 startPos
     if !initText.trim.isEmpty then
       -- If there is a header comment, preserve it and put `module` in the line after
       initText := initText.trimRight ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract startPos text.endPos
+    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
 
     IO.FS.writeFile path text

script/Shake.lean

@@ -563,14 +563,14 @@ def main (args : List String) : IO UInt32 := do
       if remove.contains mod || seen.contains mod then
         out := out ++ text.extract pos stx.raw.getPos?.get!
         -- We use the end position of the syntax, but include whitespace up to the first newline
-        pos := text.findAux (· == '\n') text.endPos stx.raw.getTailPos?.get! + ⟨1⟩
+        pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + ⟨1⟩
       seen := seen.insert mod
     out := out ++ text.extract pos insertion
     for mod in add do
       if !seen.contains mod then
         seen := seen.insert mod
         out := out ++ s!"{mod}\n"
-    out := out ++ text.extract insertion text.endPos
+    out := out ++ text.extract insertion text.rawEndPos
 
     IO.FS.writeFile path out
     return count + 1

src/Init/Data/Format/Basic.lean

@@ -170,7 +170,7 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
   | text s,       flatten, _, _ =>
     let p := String.Internal.posOf s '\n'
     let off := String.Internal.offsetOfPos s p
-    { foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
+    { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && 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
@@ -264,14 +264,14 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
     | nest n f => be w (gs' ({ i with f, indent := i.indent + n }::is))
     | text s =>
       let p := String.Internal.posOf s '\n'
-      if p == s.endPos then
+      if p == s.rawEndPos then
         pushOutput s
         endTags i.activeTags
         be w (gs' is)
       else
         pushOutput (String.Internal.extract s {} p)
         pushNewline i.indent.toNat
-        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.endPos) }::is
+        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

src/Init/Data/String/Basic.lean

@@ -1550,7 +1550,7 @@ def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term
 
 def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
   match stx.raw[1] with
-  | Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.endPos ⟨2⟩)
+  | Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.rawEndPos ⟨2⟩)
   | _                 => ""
 
 end TSyntax

src/Init/Meta/Defs.lean

@@ -3441,7 +3441,7 @@ Character positions (counting the Unicode code points rather than bytes) are rep
 `Nat`s. Indexing a `String` by a `String.Pos.Raw` takes constant time, while character positions need to
 be translated internally to byte positions, which takes linear time.
 
-A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p` lies on a UTF-8
+A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.rawEndPos` and `p` lies on a UTF-8
 character boundary, see `String.Pos.IsValid`.
 
 There is another type, `String.ValidPos`, which bundles the validity predicate. Using `String.ValidPos`
@@ -3501,10 +3501,10 @@ def String.utf8ByteSize (s : @& String) : Nat :=
 /--
 A UTF-8 byte position that points at the end of a string, just after the last character.
 
-* `"abc".endPos = ⟨3⟩`
-* `"L∃∀N".endPos = ⟨8⟩`
+* `"abc".rawEndPos = ⟨3⟩`
+* `"L∃∀N".rawEndPos = ⟨8⟩`
 -/
-@[inline] def String.endPos (s : String) : String.Pos.Raw where
+@[inline] def String.rawEndPos (s : String) : String.Pos.Raw where
   byteIdx := utf8ByteSize s
 
 /--
@@ -3513,7 +3513,7 @@ Converts a `String` into a `Substring` that denotes the entire string.
 @[inline] def String.toSubstring (s : String) : Substring where
   str      := s
   startPos := {}
-  stopPos  := s.endPos
+  stopPos  := s.rawEndPos
 
 /--
 Converts a `String` into a `Substring` that denotes the entire string.

src/Init/Prelude.lean

@@ -153,7 +153,7 @@ directory.
 -/
 def fileName (p : FilePath) : Option String :=
   let lastPart := match posOfLastSep p with
-    | some sepPos => String.Pos.Raw.extract p.toString (sepPos + '/') p.toString.endPos
+    | some sepPos => String.Pos.Raw.extract p.toString (sepPos + '/') p.toString.rawEndPos
     | none        => p.toString
   if lastPart.isEmpty || lastPart == "." || lastPart == ".." then none else some lastPart
 
@@ -192,7 +192,7 @@ def extension (p : FilePath) : Option String :=
   p.fileName.bind fun fname =>
     match fname.revPosOf '.' with
     | some 0   => none
-    | some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.endPos
+    | some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.rawEndPos
     | none     => none
 
 /--

src/Init/System/FilePath.lean

@@ -111,10 +111,10 @@ instance : FromJson CompletionIdentifier where
     | .str s =>
       let c := s.front
       if c == 'c' then
-        let declName := String.Pos.Raw.extract s ⟨1⟩ s.endPos |>.toName
+        let declName := String.Pos.Raw.extract s ⟨1⟩ s.rawEndPos |>.toName
         .ok <| .const declName
       else if c == 'f' then
-        let id := ⟨String.Pos.Raw.extract s ⟨1⟩ s.endPos |>.toName⟩
+        let id := ⟨String.Pos.Raw.extract s ⟨1⟩ s.rawEndPos |>.toName⟩
         .ok <| .fvar id
       else
         .error "Expected string with prefix `c` or `f` in `FromJson` instance of `CompletionIdentifier`."

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -66,8 +66,8 @@ def parseVersoDocString
 
   -- Skip trailing `-/`
   let endPos := String.Pos.Raw.prev text.source <| endPos.prev text.source
-  let endPos := if endPos ≤ text.source.endPos then endPos else text.source.endPos
-  have endPos_valid : endPos ≤ text.source.endPos := by
+  let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos
+  have endPos_valid : endPos ≤ text.source.rawEndPos := by
     unfold endPos
     split <;> simp [*]
 

src/Lean/DocString/Add.lean

@@ -210,11 +210,11 @@ def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array Module
 def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
   match stx.raw[1] with
   | Syntax.atom _ val =>
-    return String.Pos.Raw.extract val 0 (val.endPos.unoffsetBy ⟨2⟩)
+    return String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩)
   | Syntax.node _ `Lean.Parser.Command.versoCommentBody _ =>
     match stx.raw[1][0] with
     | Syntax.atom _ val =>
-      return String.Pos.Raw.extract val 0 (val.endPos.unoffsetBy ⟨2⟩)
+      return String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩)
     | _ =>
       throwErrorAt stx "unexpected doc string{indentD stx}"
   | _ =>