chore: rename String.Range to Lean.Syntax.Range (#10852)

This PR renames `String.Range` to `Lean.Syntax.Range`, to reflect that
it is not part of the standard library.

Author: TwoFX

src/Lean/Data/Lsp/Utf16.lean

@@ -89,15 +89,15 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos.Raw) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)
 
-/-- Gets the LSP range from a `String.Range`. -/
-def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
+/-- Gets the LSP range from a `Lean.Syntax.Range`. -/
+def utf8RangeToLspRange (text : FileMap) (range : Lean.Syntax.Range) : Lsp.Range :=
   { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
 
 /-- Gets the LSP range of syntax `stx`. -/
 def lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly := false) : Option Lsp.Range :=
   text.utf8RangeToLspRange <$> stx.getRange? canonicalOnly
 
-def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range :=
+def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : Lean.Syntax.Range :=
   { start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }
 
 end FileMap

src/Lean/DocString/Links.lean

@@ -100,7 +100,7 @@ environment variable. If this environment variable is not set, a manual root pro
 built is used (typically this is the version corresponding to the current release). If no such root
 is available, the latest version of the manual is used.
 -/
-def rewriteManualLinksCore (s : String) : BaseIO (Array (String.Range × String) × String) := do
+def rewriteManualLinksCore (s : String) : BaseIO (Array (Lean.Syntax.Range × String) × String) := do
   let scheme := "lean-manual://"
   let mut out := ""
   let mut errors := #[]

src/Lean/Elab/DocString/Builtin.lean

@@ -122,7 +122,7 @@ private def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m St
   else
     throwError "Expected precisely 1 code argument"
 
-private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m String.Range := do
+private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m Lean.Syntax.Range := do
   let pos := (s.raw.getPos? (canonicalOnly := true)).get!
   let endPos := s.raw.getTailPos? true |>.get!
   return ⟨pos, endPos⟩

src/Lean/Elab/DocString/Builtin/Parsing.lean

@@ -13,7 +13,7 @@ open Lean.Parser
 
 public section
 
-private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m String.Range := do
+private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m Lean.Syntax.Range := do
   let pos := (s.raw.getPos? (canonicalOnly := true)).get!
   let endPos := s.raw.getTailPos? true |>.get!
   return ⟨pos, endPos⟩

src/Lean/Elab/InfoTree/InlayHints.lean

@@ -16,7 +16,7 @@ open Lean
 
 structure InlayHintLinkLocation where
   module : Name
-  range  : String.Range
+  range  : Lean.Syntax.Range
 
 structure InlayHintLabelPart where
   value     : String
@@ -32,7 +32,7 @@ inductive InlayHintKind where
   | parameter
 
 structure InlayHintTextEdit where
-  range   : String.Range
+  range   : Lean.Syntax.Range
   newText : String
   deriving BEq
 

src/Lean/Language/Basic.lean

@@ -74,7 +74,7 @@ inductive SnapshotTask.ReportingRange where
   /-- Inherit range from outer task if any, or else the entire file. -/
   | inherit
   /-- Use given range. -/
-  | protected some (range : String.Range)
+  | protected some (range : Lean.Syntax.Range)
   /-- Do not mark as being processed. Child nodes are still visited. -/
   | skip
 deriving Inhabited
@@ -83,7 +83,7 @@ deriving Inhabited
 Constructs a reporting range by replacing a missing range with `inherit`, which is a reasonable
 default to ensure that a range is shown in all cases.
 -/
-def SnapshotTask.ReportingRange.ofOptionInheriting : Option String.Range → SnapshotTask.ReportingRange
+def SnapshotTask.ReportingRange.ofOptionInheriting : Option Lean.Syntax.Range → SnapshotTask.ReportingRange
   | some range => .some range
   | none       => .inherit
 

src/Lean/Linter/ConstructorAsVariable.lean

@@ -38,7 +38,7 @@ def constructorNameAsVariable : Linter where
       | return
 
     let infoTrees := (← get).infoState.trees.toArray
-    let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
+    let warnings : IO.Ref (Std.HashMap Lean.Syntax.Range (Syntax × Name × Name)) ← IO.mkRef {}
 
     for tree in infoTrees do
       tree.visitM' (postNode := fun ci info _ => do

src/Lean/Linter/UnusedSimpArgs.lean

@@ -46,7 +46,7 @@ def unusedSimpArgs : Linter where
     let some cmdStxRange := cmdStx.getRange?  | return
 
     let infoTrees := (← get).infoState.trees.toArray
-    let masksMap : IO.Ref (Std.HashMap String.Range (Syntax × Array Bool)) ← IO.mkRef {}
+    let masksMap : IO.Ref (Std.HashMap Lean.Syntax.Range (Syntax × Array Bool)) ← IO.mkRef {}
 
     for tree in infoTrees do
       tree.visitM' (postNode := fun ci info _ => do

src/Lean/Linter/UnusedVariables.lean

@@ -369,11 +369,11 @@ structure References where
   the spans for `foo`, `bar`, and `baz`. Global definitions are always treated as used.
   (It would be nice to be able to detect unused global definitions but this requires more
   information than the linter framework can provide.) -/
-  constDecls : Std.HashSet String.Range := ∅
+  constDecls : Std.HashSet Lean.Syntax.Range := ∅
   /-- The collection of all local declarations, organized by the span of the declaration.
   We collapse all declarations declared at the same position into a single record using
   `FVarDefinition.aliases`. -/
-  fvarDefs : Std.HashMap String.Range FVarDefinition := ∅
+  fvarDefs : Std.HashMap Lean.Syntax.Range FVarDefinition := ∅
   /-- The set of `FVarId`s that are used directly. These may or may not be aliases. -/
   fvarUses : Std.HashSet FVarId := ∅
   /-- A mapping from alias to original FVarId. We don't guarantee that the value is not itself
@@ -386,7 +386,7 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range)
+partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : Lean.Syntax.Range)
     (linterSets : LinterSets) :
     StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
 where

src/Lean/Linter/Util.lean

@@ -22,7 +22,7 @@ The result is `some []` if no `MacroExpansionInfo` was found on the way and
 
 Return the result reversed, s.t. the macro expansion that would be applied to
 the original syntax first is the first element of the returned list. -/
-def collectMacroExpansions? {m} [Monad m] (range : String.Range) (tree : Elab.InfoTree) : m <| Option <| List Elab.MacroExpansionInfo := do
+def collectMacroExpansions? {m} [Monad m] (range : Lean.Syntax.Range) (tree : Elab.InfoTree) : m <| Option <| List Elab.MacroExpansionInfo := do
   if let .some <| .some result ← go then
     return some result.reverse
   else