# Documentation

Lean.Server.Utils

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

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.

Like tee a | b on Unix. See chainOut.

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

Prefixes all written outputs with pre.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
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) :

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.

Returns the document contents with the change applied.

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

Returns the document contents with all changes applied.

Equations
def Lean.Server.publishDiagnostics (diagnostics : ) (hOut : IO.FS.Stream) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Server.publishProgress (processing : ) (hOut : IO.FS.Stream) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.