fix: only enable InsertReplaceEdit if supported

src/Lean/Data/Lsp/Capabilities.lean

@@ -17,15 +17,21 @@ namespace Lsp
 
 open Json
 
--- TODO: right now we ignore the client's capabilities
-inductive ClientCapabilities where
-  | mk
+structure CompletionItemCapabilities where
+  insertReplaceSupport? : Option Bool
+  deriving ToJson, FromJson
 
-instance : FromJson ClientCapabilities :=
-  ⟨fun j => ClientCapabilities.mk⟩
+structure CompletionClientCapabilities where
+  completionItem? : Option CompletionItemCapabilities
+  deriving ToJson, FromJson
 
-instance ClientCapabilities.hasToJson : ToJson ClientCapabilities :=
-  ⟨fun o => mkObj []⟩
+structure TextDocumentClientCapabilities where
+  completion? : Option CompletionClientCapabilities
+  deriving ToJson, FromJson
+
+structure ClientCapabilities where
+  textDocument? : Option TextDocumentClientCapabilities
+  deriving ToJson, FromJson
 
 -- TODO largely unimplemented
 structure ServerCapabilities where

src/Lean/Server/Completion.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Environment
 import Lean.Parser.Term
 import Lean.Data.Lsp.LanguageFeatures
+import Lean.Data.Lsp.Capabilities
 import Lean.Data.Lsp.Utf16
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Match.MatcherInfo
@@ -318,7 +319,7 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (hoverInfo : Hov
             if (← isDotCompletionMethod typeName c) then
               addCompletionItem c.name.getString! c.type expectedType? c.name (kind := (← getCompletionKindForDecl c))
 
-private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option CompletionList) :=
+private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCapabilities) : IO (Option CompletionList) :=
   ctx.runMetaM {} do
     let (partialName, trailingDot) :=
       -- `stx` is from `"set_option" >> ident`
@@ -337,7 +338,9 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option Com
     for ⟨name, decl⟩ in decls do
       if partialName.isPrefixOf name.toString then
         let textEdit :=
-          if let some ⟨start, stop⟩ := stx[1].getRange? then
+          if !caps.textDocument?.any (·.completion?.any (·.completionItem?.any (·.insertReplaceSupport?.any (·)))) then
+            none -- InsertReplaceEdit not supported by client
+          else if let some ⟨start, stop⟩ := stx[1].getRange? then
             let stop := if trailingDot then stop + 1 else stop
             let range := ⟨ctx.fileMap.utf8PosToLspPos start, ctx.fileMap.utf8PosToLspPos stop⟩
             some { newText := name.toString, insert := range, replace := range : InsertReplaceEdit }
@@ -360,14 +363,14 @@ private def tacticCompletion (ctx : ContextInfo) : IO (Option CompletionList) :=
       items.push { label := tk.toString, detail? := none, documentation? := none, kind? := CompletionItemKind.keyword }
     return some { items := sortCompletionItems items, isIncomplete := true }
 
-partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) : IO (Option CompletionList) := do
+partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) (caps : ClientCapabilities) : IO (Option CompletionList) := do
   let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
   match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with
   | some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
     match info with
     | CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
     | CompletionInfo.id stx id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
-    | CompletionInfo.option stx => optionCompletion ctx stx
+    | CompletionInfo.option stx => optionCompletion ctx stx caps
     | CompletionInfo.tactic .. => tacticCompletion ctx
     | _ => return none
   | _ =>

src/Lean/Server/FileWorker.lean

@@ -60,6 +60,7 @@ structure WorkerContext where
   hOut          : FS.Stream
   hLog          : FS.Stream
   srcSearchPath : SearchPath
+  initParams    : InitializeParams
 
 /- Asynchronous snapshot elaboration. -/
 section Elab
@@ -207,7 +208,7 @@ section Initialization
     publishDiagnostics m headerSnap.diagnostics.toArray hOut
     return (headerSnap, srcSearchPath)
 
-  def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (opts : Options)
+  def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
       : IO (WorkerContext × WorkerState) := do
     let (headerSnap, srcSearchPath) ← compileHeader meta o opts
     let cancelTk ← CancelToken.new
@@ -216,6 +217,7 @@ section Initialization
         hOut               := o
         hLog               := e
         srcSearchPath      := srcSearchPath
+        initParams         := initParams
       }
     let cmdSnaps ← unfoldCmdSnaps meta headerSnap cancelTk (initial := true) ctx
     let doc : EditableDocument := ⟨meta, headerSnap, cmdSnaps, cancelTk⟩
@@ -371,7 +373,8 @@ section MessageHandling
       { rpcSessions := st.rpcSessions
         srcSearchPath := ctx.srcSearchPath
         doc := st.doc
-        hLog := ctx.hLog }
+        hLog := ctx.hLog
+        initParams := ctx.initParams }
     let t? ← EIO.toIO' <| handleLspRequest method params rc
     let t₁ ← match t? with
       | Except.error e =>
@@ -426,7 +429,7 @@ end MainLoop
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  let _ ← i.readLspRequestAs "initialize" InitializeParams
+  let initParams ← i.readLspRequestAs "initialize" InitializeParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
@@ -438,7 +441,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let e ← e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let (ctx, st) ← initializeWorker meta i o e opts
+    let (ctx, st) ← initializeWorker meta i o e initParams.param opts
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) mainLoop
     return (0 : UInt32)
   catch e =>

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -25,13 +25,14 @@ partial def handleCompletion (p : CompletionParams)
   let doc ← readDoc
   let text := doc.meta.text
   let pos := text.lspPosToUtf8Pos p.position
+  let caps := (← read).initParams.capabilities
   -- dbg_trace ">> handleCompletion invoked {pos}"
   -- NOTE: use `+ 1` since we sometimes want to consider invalid input technically after the command,
   -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent
   -- command starts with a keyword that (currently?) does not participate in completion.
   withWaitFindSnap doc (·.endPos + 1 >= pos)
     (notFoundX := pure { items := #[], isIncomplete := true }) fun snap => do
-      if let some r ← Completion.find? doc.meta.text pos snap.infoTree then
+      if let some r ← Completion.find? doc.meta.text pos snap.infoTree caps then
         return r
       return { items := #[ ], isIncomplete := true }
 

src/Lean/Server/Requests.lean

@@ -59,6 +59,7 @@ structure RequestContext where
   srcSearchPath : SearchPath
   doc           : FileWorker.EditableDocument
   hLog          : IO.FS.Stream
+  initParams    : Lsp.InitializeParams
 
 abbrev RequestTask α := Task (Except RequestError α)
 /-- Workers execute request handlers in this monad. -/

tests/lean/interactive/run.lean

@@ -7,7 +7,16 @@ partial def main (args : List String) : IO Unit := do
   let uri := s!"file://{args.head!}"
   Ipc.runWith (←IO.appPath) #["--server"] do
     let hIn ← Ipc.stdin
-    Ipc.writeRequest ⟨0, "initialize", { capabilities := ⟨⟩ : InitializeParams }⟩
+    let capabilities := {
+      textDocument? := some {
+        completion? := some {
+          completionItem? := some {
+            insertReplaceSupport? := true
+          }
+        }
+      }
+    }
+    Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩
     let _ ← Ipc.readResponseAs 0 InitializeResult
     Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩