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
Instances For
Prefixes all written outputs with pre
.
Equations
Instances For
Meta-Data of a document.
- uri : Lsp.DocumentUri
URI where the document is located.
- mod : Name
Module name corresponding to
uri
. We store the module name instead of recomputing it as needed to ensure that we can still determine the original module name even when the file has been deleted in the mean-time. - version : Nat
Version number of the document. Incremented whenever the document is edited.
- text : FileMap
Current text of the document. It is maintained such that it is normalized using
String.crlfToLf
, which preserves logical line/column numbers. (Note: we assume that edit operations never split or merge\r\n
line endings.) - dependencyBuildMode : Lsp.DependencyBuildMode
Controls when dependencies of the document are built on
textDocument/didOpen
notifications.
Instances For
Extracts an InputContext
from doc
.
Equations
Instances For
Duplicates an I/O stream to a log file fName
in LEAN_SERVER_LOG_DIR
if that envvar is set.
Equations
Instances For
Returns the document contents with the change applied.
Equations
Instances For
Returns the document contents with all changes applied.
Equations
Instances For
Constructs a textDocument/publishDiagnostics
notification.
Equations
Instances For
Constructs a $/lean/fileProgress
notification.
Equations
Instances For
Constructs a $/lean/fileProgress
notification from the given position onwards.
Equations
Instances For
Constructs a $/lean/fileProgress
notification marking processing as done.
Equations
Instances For
Equations
Instances For
Finds the URI corresponding to modName
in searchSearchPath
.
Yields none
if the file corresponding to modName
has been deleted in the mean-time.