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

fix: server ContentChangeEvent order

Browse source
This commit is contained in:
Wojciech Nawrocki 2020-11-24 11:58:20 -05:00 • committed by Sebastian Ullrich
parent 8c4becbdd3
commit 5b613eab09
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Server/Utils.lean
View file

@ -88,8 +88,8 @@ which lands earliest in the file. Panics if there are no changes. -/
def foldDocumentChanges (changes : @& Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap)
: FileMap × String.Pos :=
if changes.isEmpty then panic! "Lean.Server.foldDocumentChanges: empty change array" else
let accumulateChanges : TextDocumentContentChangeEvent → FileMap × String.Pos → FileMap × String.Pos :=
fun change ⟨newDocText, minStartOff⟩ =>
let accumulateChanges : FileMap × String.Pos → TextDocumentContentChangeEvent → FileMap × String.Pos :=
fun ⟨newDocText, minStartOff⟩ change =>
match change with
| TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) =>
let startOff := oldText.lspPosToUtf8Pos range.start
@ -99,7 +99,7 @@ def foldDocumentChanges (changes : @& Array Lsp.TextDocumentContentChangeEvent)
| TextDocumentContentChangeEvent.fullChange (newText : String) =>
⟨newText.toFileMap, 0⟩
-- NOTE: We assume Lean files are below 16 EiB.
changes.foldr accumulateChanges (oldText, 0xffffffff)
changes.foldl accumulateChanges (oldText, 0xffffffff)
end Server
end Lean