Documentation

Lean.Server.FileWorker.RequestHandling

Handles completionItem/resolve requests that are sent by the client after the user selects a completion item that was provided by textDocument/completion. Resolving the item fills the detail? field of the item with the pretty-printed type. This control flow is necessary because pretty-printing the type for every single completion item (even those never selected by the user) is inefficient.

Equations
    Instances For
      • name : List Name

        The list of the name components introduced by this namespace command, in reverse order so that end will peel them off from the front.

      • stx : Syntax
      • selection : Syntax
      • prevSiblings : Array Lsp.DocumentSymbol
      Instances For