Skip to content

[M2] Implement textDocument/hover #23

@zacky1972

Description

@zacky1972

Summary

Expose a minimal hover query API for Lean source positions.

Tasks

  • Build textDocument/hover requests.
  • Convert line/character positions to LSP format.
  • Parse hover responses.
  • Add an integration test against the fixture project.

Acceptance criteria

  • LeanLsp.hover(session, path, line, character) returns structured hover information.
  • Hover queries work through the Docker-backed runtime.

Metadata

Metadata

Assignees

No one assigned

    Labels

    area:lspLSP, JSON-RPC, transport, and protocol supportkind:taskImplementation taskpriority:highHigh-priority task

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions