Documentation

Lean.Server.FileSource

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances

      Yields the file source of item by attempting to obtain mod : Name from item.data?.

      Panics if item.data? is not present or does not contain a mod field and the first element of a data? array cannot be parsed to Name. Used when completionItem/resolve requests pass the watchdog to decide which file worker to forward the request to. Since this function can panic and clients typically send completionItem/resolve requests for every selected completion item, all completion items returned by the server in textDocument/completion requests must have a data? field that has a mod field.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For