max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: index out of bounds

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-09 10:08:28 -07:00
parent af588078e0
commit bc8daee635
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Data/Lsp/Utf16.lean
View file

@ -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