From 048d592fe84b3b59e1ea057221a7c42ff8d001a9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 13 Mar 2021 17:51:37 +0100
Subject: [PATCH] fix: FileMap out of bounds

---
 src/Lean/Data/Position.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index a35dc0a8f3..fa520111d4 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -60,8 +60,9 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
       loop 0 (ps.size -1)
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
-      -- which would violate `toPositionAux`'s invariant
-      ⟨1, pos⟩
+      -- which would violate `toPositionAux`'s invariant.
+      -- Can also happen with EOF errors, which are not strictly inside the file.
+      ⟨lines.back, pos - ps.back⟩
 
 end FileMap
 end Lean