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
def Lean.Lsp.DocumentUri.ofPath (fname : System.FilePath) :
Lean.Lsp.DocumentUri

Transform the given path to a file:// URI.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Lsp.DocumentUri.toPath? (uri : Lean.Lsp.DocumentUri) :
Option System.FilePath

Return local path from file:// URI, if any.

Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Server.DocumentMeta:
Type
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 String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) :
Lean.Lsp.Range
Equations