diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index aa956a3..0cca9c1 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -496,7 +496,7 @@ section NotificationHandling IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}" else if ¬ changes.isEmpty then let newDocText := foldDocumentChanges changes oldDoc.meta.text - updateDocument ⟨docId.uri, newVersion, newDocText⟩ + updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩ end NotificationHandling @@ -573,7 +573,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do This is because LSP always refers to characters by (line, column), so if we get the line number correct it shouldn't matter that there is a CR there. -/ - let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩ + let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩ let e := e.withPrefix s!"[{param.textDocument.uri}] " let _ ← IO.setStderr e try diff --git a/server/Main.lean b/server/Main.lean index d18aac9..90a3e33 100644 --- a/server/Main.lean +++ b/server/Main.lean @@ -1,5 +1,9 @@ import GameServer.FileWorker import GameServer.Watchdog +import GameServer.Commands + +-- TODO: The only reason we import `Commands` is so that it gets built to on `lake build` +-- should we have a different solution? unsafe def main : List String → IO UInt32 := fun args => do let e ← IO.getStderr diff --git a/server/lean-toolchain b/server/lean-toolchain index f8f5f5c..2f868c6 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.1.0 +leanprover/lean4:v4.2.0