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

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

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")