From 45bcef5dab424cdf2d818e60476dd2b4e8079ef0 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 13 Dec 2021 20:04:39 +0100 Subject: [PATCH] refactor: server: use String.firstDiffPos to find changes This is necessary so that we do not reprocess the whole file if incremental sync is disabled. --- src/Init/Data/String/Basic.lean | 8 ++++++++ src/Lean/Server/FileWorker.lean | 10 +++++----- src/Lean/Server/Utils.lean | 27 ++++++++++----------------- src/Lean/Server/Watchdog.lean | 2 +- 4 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 8ab05886a8..fd398b1d87 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -126,6 +126,14 @@ def revFind (s : String) (p : Char → Bool) : Option Pos := if s.bsize == 0 then none else revFindAux s p (s.prev s.bsize) +/-- Returns the first position where the two strings differ. -/ +partial def firstDiffPos (a b : String) : Pos := + let stopPos := a.bsize.min b.bsize + let rec loop (i : Pos) : Pos := + if i == stopPos || a.get i != b.get i then i + else loop (a.next i) + loop 0 + private def utf8ExtractAux₂ : List Char → Pos → Pos → List Char | [], _, _ => [] | c::cs, i, e => if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index c86ad9d8c6..2a8bb00a8d 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -221,9 +221,8 @@ section Updates def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : WorkerM Unit := do modify fun st => { st with pendingRequests := map st.pendingRequests } - /-- Given the new document and `changePos`, the UTF-8 offset of a change into the pre-change source, - updates editable doc state. -/ - def updateDocument (newMeta : DocumentMeta) (changePos : String.Pos) : WorkerM Unit := do + /-- Given the new document, updates editable doc state. -/ + def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do -- The watchdog only restarts the file worker when the syntax tree of the header changes. -- If e.g. a newline is deleted, it will not restart this file worker, but we still -- need to reparse the header so that the offsets are correct. @@ -241,6 +240,7 @@ section Updates | some (ElabTaskError.ioError ioError) => throw ioError | _ => -- No error or EOF oldDoc.cancelTk.set + let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead. let mut validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos) @@ -282,8 +282,8 @@ section NotificationHandling -- TODO(WN): This happens on restart sometimes. IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}" else if ¬ changes.isEmpty then - let (newDocText, minStartOff) := foldDocumentChanges changes oldDoc.meta.text - updateDocument ⟨docId.uri, newVersion, newDocText⟩ minStartOff + let newDocText := foldDocumentChanges changes oldDoc.meta.text + updateDocument ⟨docId.uri, newVersion, newDocText⟩ def handleCancelRequest (p : CancelParams) : WorkerM Unit := do updatePendingRequests (fun pendingRequests => pendingRequests.erase p.id) diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index f8fcc7e5bb..7d0e55d3f8 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -105,23 +105,16 @@ def toFileUri (fname : System.FilePath) : Lsp.DocumentUri := open Lsp -/-- Returns the document contents with all changes applied, together with the position of the change -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 : 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 - let newDocText := replaceLspRange newDocText range newText - let minStartOff := minStartOff.min startOff - ⟨newDocText, minStartOff⟩ - | TextDocumentContentChangeEvent.fullChange (newText : String) => - ⟨newText.toFileMap, 0⟩ - -- NOTE: We assume Lean files are below 16 EiB. - changes.foldl accumulateChanges (oldText, 0xffffffff) +/-- Returns the document contents with the change applied. -/ +def applyDocumentChange (oldText : FileMap) : (change : Lsp.TextDocumentContentChangeEvent) → FileMap + | TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) => + replaceLspRange oldText range newText + | TextDocumentContentChangeEvent.fullChange (newText : String) => + newText.toFileMap + +/-- Returns the document contents with all changes applied. -/ +def foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap) : FileMap := + changes.foldl applyDocumentChange oldText def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (hOut : FS.Stream) : IO Unit := hOut.writeLspNotification { diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 44d4adb891..f2aa044e10 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -355,7 +355,7 @@ section NotificationHandling throwServerError "Got outdated version number" if changes.isEmpty then return - let (newDocText, _) := foldDocumentChanges changes oldDoc.meta.text + let newDocText := foldDocumentChanges changes oldDoc.meta.text let newMeta : DocumentMeta := ⟨doc.uri, newVersion, newDocText⟩ let newHeaderAst ← parseHeaderAst newDocText.source if newHeaderAst != oldDoc.headerAst then