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

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

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)

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 {

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