Upstream-blocked: textDocument/documentSymbol merge from Isabelle/PIDE

[Arthur742Ramos]

The Isabelle 2025-2 isabelle vscode_server LSP does not advertise textDocument/documentSymbol capability, so VS Code's Outline view and breadcrumb bar fall back to the extension's local syntax-only document-symbol provider (src/semantic/documentSymbols.ts).

This is the last remaining upstream-blocked item on the M5 (semantic markup) milestone — see docs/ROADMAP_STATUS.md "Milestone 5 — Semantic markup" (status: ✅ 8 of 9).

Impact

• The Outline view still works, but the local provider only sees what the conservative TypeScript-side parser extracts from .thy headers and command spans. It misses cross-file declarations, locale members, anonymous datatypes, and anything elaborated by Isabelle's own theory loader.
• Workaround: open examples/Smoke.thy against the bundled Isabelle_VSCode_Smoke session — the local provider surfaces the three top-level definitions (conj_commute_smoke, add_zero_right_smoke, identity_smoke) which is enough for navigation in small theories.

Resolution paths (any one closes this)

1. Upstream PR to isabelle vscode_server adding documentSymbolProvider capability + the corresponding textDocument/documentSymbol handler. Track via the Isabelle developer list.
2. Scala backend PideBridge.documentSymbols(theoryUri) that walks the Headless Document.Snapshot and emits the structured symbol list ourselves, then surfaces it via a new JSON-RPC document/symbolsWithPide method consumed by a TS provider that merges with the existing local one. This is analogous to PR feat(backend): Phase 3a — PIDE snapshot extraction + per-(uri,version,session) cache #79's proofState/getWithPide for proof state. Cost: 1–2 PRs, similar surface area to Phase 3a.

The PideBridge route (option 2) is the realistic near-term path since we already own that bridge end-to-end. The upstream PR (option 1) would be cleaner but depends on Isabelle release cadence and reviewer bandwidth we don't control.

Acceptance criteria

This issue closes when EITHER:

• The local document-symbol provider in src/semantic/documentSymbols.ts is supplemented by a PIDE-backed source that surfaces declarations elaborated by Isabelle's own loader (cross-file, locale members, etc.), OR
• Upstream Isabelle ships an LSP build that advertises documentSymbolProvider and our existing IsabelleLanguageClient wiring picks it up without further work.

References

• docs/ROADMAP_STATUS.md — milestone status.
• docs/PIDE_INTEGRATION.md — full LSP capability checklist.
• docs/proof_state_and_minimization_lsp_research.md — methodology for confirming upstream LSP gaps.
• AGENTS.md §11 — PIDE classpath bridge (would underpin option 2).

[Arthur742Ramos]

Pre-implementation design refinement based on a rubber-duck pass run while scoping this issue alongside the now-merged Phase 3c (#92, PR #94).

Critical course-correction: regex-over-cmd.source is not "PIDE-elaborated"

The naive approach — walk snapshot.node.commands, regex-extract names from cmd.source for a fixed set of declaration keywords — has been rejected as ineffective for closing this issue.

Reasons:

• It mostly reproduces the existing local syntax provider (src/semantic/documentSymbols.ts) with a much more expensive PIDE-backed code path.
• It misses or mishandles every shape that needs PIDE elaboration to resolve correctly:
  • Multiple declarations: consts a :: ... and b :: ...
  • Mutual definitions: fun f ... and g ...
  • Attributes before/after names: theorem [simp, intro] foo : "..."
  • Qualified / private / local declarations
  • Custom commands from sessions / AFP entries
  • Commands whose first identifier is not the declared entity
• Brittle in the way the local provider is brittle, just slower.

If the goal is "close M5 documentSymbol gap with the local provider as fallback", PIDE has to give us declared entities from its own elaboration — not from source-text parsing.

Recommended architecture (still requires live investigation)

1. Symbol source: PIDE entity markup, not cmd.source regex

Investigate Isabelle's Markup.ENTITY (and related Markup.DECLARATION / Markup.DEFINITION / Markup.THEOREM) markup-aspect surfaces. The isabelle dump tool's markup aspect uses snapshot.markup_to_XML and snapshot.cumulate to gather these — see Isabelle's Markup.scala upstream for the markup taxonomy.

The reflective entry point is Document.Snapshot.cumulate[A](range, info, elements, result), which returns a stream of Text.Info[A] for the matching markup. For symbols we want positions + names + kinds; the result type would be a tuple shape we'd render to JSON-RPC.

We cannot reliably figure out the exact cumulate signature OR the markup taxonomy without a live Isabelle install at hand to probe.

2. Cache-hit-only mode — no cold builds triggered by Outline

VS Code re-requests document symbols on every edit. Triggering a cold use_theories (~20 s, single PIDE worker thread) every time the Outline view is open would block proofState/getWithPide and sledgehammer/run for the same worker.

Design contract:

document/symbolsWithPide {uri, version, session} if SnapshotCache hit for (uri, version, session): extract symbols from cached snapshot return status: "ready", symbols: [...] else: return status: "unavailable", reason: "snapshot-cache-miss" (TS side falls back silently to the local provider)

A pre-warmer (or "open Outline" command explicitly) could trigger use_theories on user request, but the routine outline-open path MUST NOT.

3. Composite TS-side provider (avoid duplicate outline entries)

Two registerDocumentSymbolProvider calls for the same selector produce duplicated entries — VS Code does not dedupe by name + range. Use one composite provider:

s class IsabelleCompositeDocumentSymbolProvider implements vscode.DocumentSymbolProvider { async provideDocumentSymbols(document, token) { const pide = await tryPideSymbolsCacheOnly(document, token); if (pide?.length) return pide; // PIDE-first return localProvider.provideDocumentSymbols(document, token); } }

The TS layer can additionally cache the PIDE result per (uri, version) so repeated outline opens within a single document version don't re-dispatch.

4. Selection ranges in symbols, not just command ranges

vscode.DocumentSymbol distinguishes the full range and the selection range (the identifier's range). For UX, the symbol's selection range should point at the declared name, not the whole command — otherwise clicking the outline entry jumps the cursor to the start of theorem instead of conj_commute_smoke.

This requires PIDE to give us the entity's name position, which the markup aspect should (modulo verification on a live install).

Open questions that need live Isabelle to answer

1. Exact reflective signature of Document.Snapshot.cumulate. Multiple overloads exist upstream; the right one for our purpose is the one returning Text.Info[T] for a given markup-element predicate.
2. Markup taxonomy: which exact Markup.NAME values correspond to user-visible declarations? Markup.ENTITY, Markup.DECLARATION, Markup.THEOREM, Markup.DEFINITION, others?
3. Per-keyword vscode.SymbolKind mapping: theorem / lemma → SymbolKind.Method? definition → SymbolKind.Variable? Local provider's mapping in src/semantic/documentSymbols.ts is a starting point but may need PIDE-aware refinement.

Acceptance criteria (revised)

• New PideDocumentSymbolExtractor calls snapshot.cumulate reflectively against an appropriate markup element set; returns Seq[(name, kind, fullRange, selectionRange)].
• New DocumentSymbolWithPideHandler operates in cache-hit-only mode: never triggers a cold use_theories. Cache miss → status: "unavailable", reason: "snapshot-cache-miss" so the TS composite provider falls back to the local one.
• TS composite provider replaces the dual-registration approach. PIDE-first, local fallback. Per-(uri, version) cache.
• Structural tests (synthetic snapshot fake) for the cache-hit path AND the cache-miss path.
• Live verification on examples/Smoke.thy: outline shows conj_commute_smoke, add_zero_right_smoke, identity_smoke with correct selection ranges. Confirm no cold use_theories is triggered by opening the outline.
• Update docs/PIDE_INTEGRATION.md (mark documentSymbol as resolved-via-bridge), docs/ROADMAP_STATUS.md Milestone 5 row (✅ 8 of 9 → ✅ 9 of 9), AGENTS.md (new gotcha if one emerges).

Why this isn't being done in the current sweep

The Phase 3c PR (#94) landed with confidence because its surface — filtering an existing reflective result by a pure predicate — was self-contained, well-tested in structural fakes, and low-risk to live Isabelle behavior.

documentSymbol is genuinely different: it needs to discover what shape snapshot.cumulate returns for the various markup-aspect overloads, which we can't reliably determine without a live Isabelle install at hand. Implementing it autonomously with regex-over-source as a stopgap would either ship the wrong thing (duplicating the local provider) OR force a follow-up rewrite once the live PIDE shape is known.

Picking this up requires either:

• A contributor with a working Isabelle install who can probe snapshot.cumulate interactively (the live backend/scripts/live-smoke-phase2a.js pattern is a starting point).
• An upstream change to isabelle vscode_server adding documentSymbolProvider (option 1 from the original issue body).

This issue stays open with the design above as the authoritative starting point for whoever picks it up.