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

Throws an IO.userError.

def IO.FS.Stream.chainRight (a b : Stream) (flushEagerly : Bool := false) : Stream

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.

def IO.FS.Stream.chainLeft (a b : Stream) (flushEagerly : Bool := false) : Stream

Like tee a | b on Unix. See chainOut.

def IO.FS.Stream.withPrefix (a : Stream) (pre : String) : Stream

Prefixes all written outputs with pre.

structure Lean.Server.DocumentMeta : Type

Meta-Data of a document.

• uri : Lsp.DocumentUri

  URI where the document is located.

• mod : Name

  Module name corresponding to uri. We store the module name instead of recomputing it as needed to ensure that we can still determine the original module name even when the file has been deleted in the mean-time.

• version : Nat

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

• text : FileMap

  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 : Lsp.DependencyBuildMode

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

instance Lean.Server.instInhabitedDocumentMeta : Inhabited DocumentMeta

def Lean.Server.DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext

Extracts an InputContext from doc.

def Lean.Server.replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap

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

def Lean.Server.maybeTee (fName : String) (isOut : Bool) (h : IO.FS.Stream) : IO IO.FS.Stream

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

def Lean.Server.applyDocumentChange (oldText : FileMap) (change : Lsp.TextDocumentContentChangeEvent) : FileMap

Returns the document contents with the change applied.

def Lean.Server.foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap) : FileMap

Returns the document contents with all changes applied.

def Lean.Server.mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) : JsonRpc.Notification Lsp.PublishDiagnosticsParams

Constructs a textDocument/publishDiagnostics notification.

def Lean.Server.mkFileProgressNotification (m : DocumentMeta) (processing : Array Lsp.LeanFileProgressProcessingInfo) : JsonRpc.Notification Lsp.LeanFileProgressParams

Constructs a $/lean/fileProgress notification.

def Lean.Server.mkFileProgressAtPosNotification (m : DocumentMeta) (pos : String.Pos) (kind : Lsp.LeanFileProgressKind := Lsp.LeanFileProgressKind.processing) : JsonRpc.Notification Lsp.LeanFileProgressParams

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

def Lean.Server.mkFileProgressDoneNotification (m : DocumentMeta) : JsonRpc.Notification Lsp.LeanFileProgressParams

Constructs a $/lean/fileProgress notification marking processing as done.

def Lean.Server.mkApplyWorkspaceEditRequest (params : Lsp.ApplyWorkspaceEditParams) : JsonRpc.Request Lsp.ApplyWorkspaceEditParams

def Lean.Server.documentUriFromModule? (modName : Name) : IO (Option Lsp.DocumentUri)

Finds the URI corresponding to modName in searchSearchPath. Yields none if the file corresponding to modName has been deleted in the mean-time.

def Lean.Server.moduleFromDocumentUri (uri : Lsp.DocumentUri) : IO Name

Finds the module name corresponding to uri in srcSearchPath.

def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range

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