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

Throws an IO.userError.

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

Meta-Data of a document.

• uri : Lean.Lsp.DocumentUri

  URI where the document is located.

• version : Nat

  Version number of the document. Incremented whenever the document is edited.

• text : Lean.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 : Lean.Lsp.DependencyBuildMode

  Controls when dependencies of the document are built on textDocument/didOpen notifications.

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

Extracts an InputContext from doc.

Equations

• doc.mkInputContext = { input := doc.text.source, fileName := ((System.Uri.fileUriToPath? doc.uri).getD { toString := doc.uri }).toString, fileMap := doc.text }

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

Replaces the range r (using LSP UTF-16 positions) in text (using UTF-8 positions) with newText.

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.mkPublishDiagnosticsNotification (m : Lean.Server.DocumentMeta) (diagnostics : Array Lean.Lsp.Diagnostic) : Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams

Constructs a textDocument/publishDiagnostics notification.

Equations

• Lean.Server.mkPublishDiagnosticsNotification m diagnostics = { method := "textDocument/publishDiagnostics", param := { uri := m.uri, version? := some ↑m.version, diagnostics := diagnostics } }

def Lean.Server.mkFileProgressNotification (m : Lean.Server.DocumentMeta) (processing : Array Lean.Lsp.LeanFileProgressProcessingInfo) : Lean.JsonRpc.Notification Lean.Lsp.LeanFileProgressParams

Constructs a $/lean/fileProgress notification.

Equations

• Lean.Server.mkFileProgressNotification m processing = { method := "$/lean/fileProgress", param := { textDocument := { uri := m.uri, version? := some m.version }, processing := processing } }

def Lean.Server.mkFileProgressAtPosNotification (m : Lean.Server.DocumentMeta) (pos : String.Pos) (kind : optParam Lean.Lsp.LeanFileProgressKind Lean.Lsp.LeanFileProgressKind.processing) : Lean.JsonRpc.Notification Lean.Lsp.LeanFileProgressParams

Constructs a $/lean/fileProgress notification from the given position onwards.

Equations

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

def Lean.Server.mkFileProgressDoneNotification (m : Lean.Server.DocumentMeta) : Lean.JsonRpc.Notification Lean.Lsp.LeanFileProgressParams

Constructs a $/lean/fileProgress notification marking processing as done.

Equations

• Lean.Server.mkFileProgressDoneNotification m = Lean.Server.mkFileProgressNotification m #[]

def Lean.Server.mkApplyWorkspaceEditRequest (params : Lean.Lsp.ApplyWorkspaceEditParams) : Lean.JsonRpc.Request Lean.Lsp.ApplyWorkspaceEditParams

Equations

• Lean.Server.mkApplyWorkspaceEditRequest params = { id := Lean.JsonRpc.RequestID.str "workspace/applyEdit", method := "workspace/applyEdit", param := params }

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

Converts an UTF-8-based String.range in text to an equivalent LSP UTF-16-based Lsp.Range in text.

Equations

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

def System.SearchPath.searchModuleNameOfUri (srcSearchPath : Lake.SearchPath) (uri : Lean.Lsp.DocumentUri) : IO (Option Lake.Name)

Attempts to find a module name in the roots denoted by srcSearchPath for uri. Fails if uri is not a file:// uri or if the given uri cannot be found in srcSearchPath.

Equations

• srcSearchPath.searchModuleNameOfUri uri = match System.Uri.fileUriToPath? uri with | some path => Lean.searchModuleNameOfFileName path srcSearchPath | x => pure none