Totally broken state

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/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,8 +3501,8 @@ 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.rawEndPos (s : String) : String.Pos.Raw where
   byteIdx := utf8ByteSize s
@@ -4718,7 +4718,7 @@ inductive SourceInfo where
   The `leading` whitespace is inferred after parsing by `Syntax.updateLeading`. This is because the
   “preceding token” is not well-defined during parsing, especially in the presence of backtracking.
   -/
-  | original (leading : Substring) (pos : String.Pos.Raw) (trailing : Substring) (endPos : String.Pos.Raw)
+  | original (leading : Substring) (pos : String.Pos.Raw) (trailing : Substring) (rawEndPos : String.Pos.Raw)
   /--
   Synthetic syntax is syntax that was produced by a metaprogram or by Lean itself (e.g. by a
   quotation). Synthetic syntax is annotated with a source span from the original syntax, which
@@ -4742,7 +4742,7 @@ inductive SourceInfo where
   ```
   In these cases, if the user hovers over `h` they will see information about both binding sites.
   -/
-  | synthetic (pos : String.Pos.Raw) (endPos : String.Pos.Raw) (canonical := false)
+  | synthetic (pos : String.Pos.Raw) (rawEndPos : String.Pos.Raw) (canonical := false)
   /-- A synthesized token without position information. -/
   | protected none
 
@@ -4769,9 +4769,9 @@ will also return `none`.
 -/
 def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos.Raw :=
   match info, canonicalOnly with
-  | original (endPos := endPos) ..,  _
-  | synthetic (endPos := endPos) (canonical := true) .., _
-  | synthetic (endPos := endPos) .., false => some endPos
+  | original (rawEndPos := rawEndPos) ..,  _
+  | synthetic (rawEndPos := rawEndPos) (canonical := true) .., _
+  | synthetic (rawEndPos := rawEndPos) .., false => some rawEndPos
   | _,                               _     => none
 
 /--
@@ -5152,15 +5152,15 @@ position information.
 -/
 partial def getTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos.Raw :=
   match stx, canonicalOnly with
-  | atom (SourceInfo.original (endPos := pos) ..) .., _
-  | atom (SourceInfo.synthetic (endPos := pos) (canonical := true) ..) _, _
-  | atom (SourceInfo.synthetic (endPos := pos) ..) _,  false
-  | ident (SourceInfo.original (endPos := pos) ..) .., _
-  | ident (SourceInfo.synthetic (endPos := pos) (canonical := true) ..) .., _
-  | ident (SourceInfo.synthetic (endPos := pos) ..) .., false
-  | node (SourceInfo.original (endPos := pos) ..) .., _
-  | node (SourceInfo.synthetic (endPos := pos) (canonical := true) ..) .., _
-  | node (SourceInfo.synthetic (endPos := pos) ..) .., false => some pos
+  | atom (SourceInfo.original (rawEndPos := pos) ..) .., _
+  | atom (SourceInfo.synthetic (rawEndPos := pos) (canonical := true) ..) _, _
+  | atom (SourceInfo.synthetic (rawEndPos := pos) ..) _,  false
+  | ident (SourceInfo.original (rawEndPos := pos) ..) .., _
+  | ident (SourceInfo.synthetic (rawEndPos := pos) (canonical := true) ..) .., _
+  | ident (SourceInfo.synthetic (rawEndPos := pos) ..) .., false
+  | node (SourceInfo.original (rawEndPos := pos) ..) .., _
+  | node (SourceInfo.synthetic (rawEndPos := pos) (canonical := true) ..) .., _
+  | node (SourceInfo.synthetic (rawEndPos := pos) ..) .., false => some pos
   | node _ _ args, _ =>
     let rec loop (i : Nat) : Option String.Pos.Raw :=
       match decide (LT.lt i args.size) with

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}"
   | _ =>

src/Lean/DocString/Extension.lean

@@ -152,7 +152,7 @@ where
   Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`.
   -/
   lookingAt (goal : String) (iter : String.Iterator) : Bool :=
-    String.Pos.Raw.substrEq iter.s iter.i goal 0 goal.endPos.byteIdx
+    String.Pos.Raw.substrEq iter.s iter.i goal 0 goal.rawEndPos.byteIdx
 
 /--
 Rewrites Lean reference manual links in `docstring` to point at the reference manual.