From bc8daee635c0ce4c3eb68aad958bbe7bea4f4ea1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 9 Apr 2021 10:08:28 -0700
Subject: [PATCH] fix: index out of bounds

---
 src/Lean/Data/Lsp/Utf16.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index 40f6497c0b..80c18e6c9c 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -65,7 +65,13 @@ namespace FileMap
 /-- 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 := text.positions.get! (pos.line)
+  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