Documentation

Lean.Server.Utils

def IO.throwServerError {α : Type} (err : String) :
IO α

Throws an IO.userError.

Equations

Chains two streams by creating a new stream s.t. writing to it just writes to a but reading from it also duplicates the read output into b, c.f. a | tee b on Unix. NB: if a is written to but this stream is never read from, the output will not be duplicated. Use this if you only care about the data that was actually read.

Equations
  • One or more equations did not get rendered due to their size.
def IO.FS.Stream.chainLeft (a b : IO.FS.Stream) (flushEagerly : Bool := false) :

Like tee a | b on Unix. See chainOut.

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

Prefixes all written outputs with pre.

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

Meta-Data of a document.

  • URI where the document is located.

  • version : Nat

    Version number of the document. Incremented whenever the document is edited.

  • Current text of the document. It is maintained such that it is normalized using String.crlfToLf, which preserves logical line/column numbers. (Note: we assume that edit operations never split or merge \r\n line endings.)

  • dependencyBuildMode : Lean.Lsp.DependencyBuildMode

    Controls when dependencies of the document are built on textDocument/didOpen notifications.

Instances For
Equations

Extracts an InputContext from doc.

Equations
  • doc.mkInputContext = { input := doc.text.source, fileName := ((System.Uri.fileUriToPath? doc.uri).getD { toString := doc.uri }).toString, fileMap := doc.text }

Replaces the range r (using LSP UTF-16 positions) in text (using UTF-8 positions) with newText.

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

Duplicates an I/O stream to a log file fName in LEAN_SERVER_LOG_DIR if that envvar is set.

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

Returns the document contents with all changes applied.

Equations

Constructs a textDocument/publishDiagnostics notification.

Equations

Constructs a $/lean/fileProgress notification.

Equations

Constructs a $/lean/fileProgress notification from the given position onwards.

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

Converts an UTF-8-based String.range in text to an equivalent LSP UTF-16-based Lsp.Range in text.

Equations

Attempts to find a module name in the roots denoted by srcSearchPath for uri. Fails if uri is not a file:// uri or if the given uri cannot be found in srcSearchPath.