Documentation

Lean.Server.Utils

source
def IO.throwServerError {α : Type} (err : String) :
IO α
Equations
source
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.
source
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.
source
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.
source
structure Lean.Server.DocumentMeta :
Type
Instances For
    source
    instance Lean.Server.instInhabitedDocumentMeta :
    Inhabited Lean.Server.DocumentMeta
    Equations
    source
    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.
    source
    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.
    source
    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.
    source
    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.
    source
    def Lean.Server.foldDocumentChanges (changes : Array Lean.Lsp.TextDocumentContentChangeEvent) (oldText : Lean.FileMap) :
    Lean.FileMap

    Returns the document contents with all changes applied.

    Equations
    source
    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.
    source
    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.
    source
    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.
    source
    def Lean.Server.publishProgressDone (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) :
    IO Unit
    Equations
    source
    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.
    source
    def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) :
    Lean.Lsp.Range
    Equations