From ea53f110274c746e376a79084bb3b4a84d5869f8 Mon Sep 17 00:00:00 2001
From: TermiNexus <wyt18222152539wyt@163.com>
Date: Wed, 28 Oct 2026 15:22:01 +0800
Subject: [PATCH] fix(lsp): honor disablePullDiagnostics and add stale-overflow
 regression

initializeOptions.disablePullDiagnostics now hides diagnosticProvider and keeps push diagnostics, matching the extension setting. gate2 verifies push and pull both clear the overflow diagnostic after the literal is fixed, and that the disable option falls back to push.
---
 App/lib/lsp/LspServer.vp | 17 ++++++++++++++---
 Tools/lsp/probe.py       | 22 ++++++++++++++++++++++
 2 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/App/lib/lsp/LspServer.vp b/App/lib/lsp/LspServer.vp
index 82fba53..cc01e7c 100644
--- a/App/lib/lsp/LspServer.vp
+++ b/App/lib/lsp/LspServer.vp
@@ -36,6 +36,9 @@ _cancel_str: list[str]* = None
 # 1 when the client advertises pull diagnostics (`textDocument.diagnostic`). Pushing
 # publishDiagnostics as well would show every problem twice in the Problems panel.
 _pull_diagnostics: int = 0
+# The extension exposes `vipeye.disablePullDiagnostics`; when set, it must not advertise
+# diagnosticProvider at all (otherwise vscode-languageclient pulls regardless).
+_disable_pull_option: int = 0
 
 
 def _CancelAdd(pool: memhub.MemManager*, id_node: json.JsonValue*):
@@ -138,7 +141,7 @@ def _BuildInitializeResult(pool: memhub.MemManager*) -> json.JsonValue*:
     if sem is not None:
         json.object_set(pool, caps, "semanticTokensProvider", sem)
     diag: json.JsonValue* = json.object(pool)
-    if diag is not None:
+    if diag is not None and _disable_pull_option == 0:
         json.object_set(pool, diag, "interFileDependencies", json.bool_val(pool, False))
         json.object_set(pool, diag, "workspaceDiagnostics", json.bool_val(pool, False))
         json.object_set(pool, caps, "diagnosticProvider", diag)
@@ -166,8 +169,16 @@ def _ClientSupportsPull(params: json.JsonValue*) -> int:
 def _HandleInitialize(pool: memhub.MemManager*, tr: LspTransport.LspTransport*,
                       ws: LspWorkspace.LspWorkspace*, id_node: json.JsonValue*,
                       params: json.JsonValue*) -> int:
-    global _pull_diagnostics
-    _pull_diagnostics = _ClientSupportsPull(params)
+    global _pull_diagnostics, _disable_pull_option
+    init_opts: json.JsonValue* = None
+    if params is not None:
+        init_opts = params["initializationOptions"]
+    _disable_pull_option = 0
+    if init_opts is not None:
+        _disable_pull_option = LspRpc.GetIntField(init_opts, "disablePullDiagnostics", 0)
+    _pull_diagnostics = 0
+    if _disable_pull_option == 0:
+        _pull_diagnostics = _ClientSupportsPull(params)
     root_uri: str = None
     if params is not None:
         root_uri = LspRpc.GetStringField(params, "rootUri")
diff --git a/Tools/lsp/probe.py b/Tools/lsp/probe.py
index 826e4bc..f011ec1 100644
--- a/Tools/lsp/probe.py
+++ b/Tools/lsp/probe.py
@@ -481,6 +481,28 @@ def gate2(exe: str) -> int:
     pull_client.request("shutdown")
     pull_client.close()
 
+    # `vipeye.disablePullDiagnostics` must hide diagnosticProvider and fall back to push.
+    push_client = Client(exe)
+    init = push_client.request(
+        "initialize",
+        {"processId": os.getpid(), "rootUri": root.as_uri(),
+         "capabilities": {"textDocument": {"diagnostic": {}}},
+         "initializationOptions": {"disablePullDiagnostics": True}},
+    )
+    caps = init.get("result", {}).get("capabilities", {})
+    if "diagnosticProvider" in caps:
+        raise AssertionError(f"disablePullDiagnostics still advertises pull: {init}")
+    push_client.notify("initialized", {})
+    push_client.notify(
+        "textDocument/didOpen",
+        {"textDocument": {"uri": uri, "languageId": "viper", "version": 6, "text": overflow}},
+    )
+    publish = push_client.wait_notification("textDocument/publishDiagnostics")
+    if len(publish.get("params", {}).get("diagnostics", [])) != 1:
+        raise AssertionError(f"disablePullDiagnostics did not push: {publish}")
+    push_client.request("shutdown")
+    push_client.close()
+
     print("diagnostics: OK")
     print("recovery: OK")
     print("overflow-diagnostics: OK")