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

def IO.FS.Stream.chainRight (a : IO.FS.Stream) (b : IO.FS.Stream) (flushEagerly : optParam Bool false) : IO.FS.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 : IO.FS.Stream) (b : IO.FS.Stream) (flushEagerly : optParam Bool false) : IO.FS.Stream

Like tee a | b on Unix. See chainOut.

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

Prefixes all written outputs with pre.

structure Lean.Server.DocumentMeta : Type

• uri : Lean.Lsp.DocumentUri
• version : Nat
• text : Lean.FileMap

instance Lean.Server.instInhabitedDocumentMeta : Inhabited Lean.Server.DocumentMeta

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

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

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 : Lean.FileMap) (change : Lean.Lsp.TextDocumentContentChangeEvent) : Lean.FileMap

Returns the document contents with the change applied.

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

Returns the document contents with all changes applied.

def Lean.Server.publishDiagnostics (m : Lean.Server.DocumentMeta) (diagnostics : Array Lean.Lsp.Diagnostic) (hOut : IO.FS.Stream) : IO Unit

def Lean.Server.publishProgress (m : Lean.Server.DocumentMeta) (processing : Array Lean.Lsp.LeanFileProgressProcessingInfo) (hOut : IO.FS.Stream) : IO Unit

def Lean.Server.publishProgressAtPos (m : Lean.Server.DocumentMeta) (pos : String.Pos) (hOut : IO.FS.Stream) (kind : optParam Lean.Lsp.LeanFileProgressKind Lean.Lsp.LeanFileProgressKind.processing) : IO Unit

def Lean.Server.publishProgressDone (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) : IO Unit

def Lean.Server.applyWorkspaceEdit (params : Lean.Lsp.ApplyWorkspaceEditParams) (hOut : IO.FS.Stream) : IO Unit

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