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

Equations

• IO.throwServerError err = throw (IO.userError err)

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.

Equations

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

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.

Equations

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

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

Prefixes all written outputs with pre.

Equations

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

structure Lean.Server.DocumentMeta : Type

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

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

Equations

• Lean.Server.instInhabitedDocumentMeta = { default := { uri := default, version := default, text := default, dependencyBuildMode := default } }

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

Equations

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

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

Equations

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

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.

Equations

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

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

Returns the document contents with the change applied.

Equations

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

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

Returns the document contents with all changes applied.

Equations

• Lean.Server.foldDocumentChanges changes oldText = Array.foldl Lean.Server.applyDocumentChange oldText changes 0

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Server.publishProgressDone m hOut = Lean.Server.publishProgress m #[] hOut

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

Equations

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

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

Equations

• String.Range.toLspRange text r = { start := Lean.FileMap.utf8PosToLspPos text r.start, end := Lean.FileMap.utf8PosToLspPos text r.stop }