better name

src/Lean/Data/Lsp/Utf16.lean

@@ -62,21 +62,24 @@ end String
 namespace Lean
 namespace FileMap
 
+private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
+  if h : line < text.positions.size then
+    text.positions.get ⟨line, h⟩
+  else if text.positions.isEmpty then
+    0
+  else
+    text.positions.back
+
 /-- Computes an UTF-8 offset into `text.source`
 from an LSP-style 0-indexed (ln, col) position. -/
 def lspPosToUtf8Pos (text : FileMap) (pos : Lsp.Position) : String.Pos :=
-  let colPos :=
-    if h : pos.line < text.positions.size then
-      text.positions.get ⟨pos.line, h⟩
-    else if text.positions.isEmpty then
-      0
-    else
-      text.positions.back
-  let chr := text.source.utf16PosToCodepointPosFrom pos.character colPos
-  text.source.codepointPosToUtf8PosFrom colPos chr
+  let lineStartPos := lineStartPos text pos.line
+  let chr := text.source.utf16PosToCodepointPosFrom pos.character lineStartPos
+  text.source.codepointPosToUtf8PosFrom lineStartPos chr
 
 def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
-  | ⟨ln, col⟩ => ⟨ln-1, text.source.codepointPosToUtf16PosFrom col (text.positions.get! $ ln - 1)⟩
+  | ⟨line, col⟩ =>
+    ⟨line - 1, text.source.codepointPosToUtf16PosFrom col (lineStartPos text (line - 1))⟩
 
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)