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 b : Stream) (flushEagerly : Bool := false) : 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 b : Stream) (flushEagerly : Bool := false) : 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 : Stream) (pre : String) : 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 : 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.

instance Lean.Server.instInhabitedDocumentMeta : Inhabited DocumentMeta

Equations

• Lean.Server.instInhabitedDocumentMeta = { default := Lean.Server.instInhabitedDocumentMeta.default }

def Lean.Server.instInhabitedDocumentMeta.default : DocumentMeta

Equations

• Lean.Server.instInhabitedDocumentMeta.default = { uri := default, mod := default, version := default, text := default, dependencyBuildMode := default }

def Lean.Server.DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext

Extracts an InputContext from doc.

Equations

• doc.mkInputContext = Lean.Parser.InputContext.mk doc.text.source ((System.Uri.fileUriToPath? doc.uri).getD { toString := doc.uri }).toString doc.text.source.rawEndPos ⋯ doc.text

def Lean.Server.replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : 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.applyDocumentChange (oldText : FileMap) (change : Lsp.TextDocumentContentChangeEvent) : FileMap

Returns the document contents with the change applied.

Equations

• Lean.Server.applyDocumentChange oldText (Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range newText) = Lean.Server.replaceLspRange oldText range newText
• Lean.Server.applyDocumentChange oldText (Lean.Lsp.TextDocumentContentChangeEvent.fullChange newText) = newText.crlfToLf.toFileMap

def Lean.Server.foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap) : FileMap

Returns the document contents with all changes applied.

Equations

• Lean.Server.foldDocumentChanges changes oldText = Array.foldl Lean.Server.applyDocumentChange oldText changes

def Lean.Server.mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) : JsonRpc.Notification 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 : DocumentMeta) (processing : Array Lsp.LeanFileProgressProcessingInfo) : JsonRpc.Notification 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 : DocumentMeta) (pos : String.Pos.Raw) (kind : Lsp.LeanFileProgressKind := Lsp.LeanFileProgressKind.processing) : JsonRpc.Notification 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 : DocumentMeta) : JsonRpc.Notification 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 : Lsp.ApplyWorkspaceEditParams) : JsonRpc.Request Lsp.ApplyWorkspaceEditParams

Equations

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

def Lean.Server.documentUriFromModule? (modName : Name) : IO (Option Lsp.DocumentUri)

Finds the URI corresponding to modName in searchSearchPath. Yields none if the file corresponding to modName has been deleted in the mean-time.

Equations

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

def Lean.Server.moduleFromDocumentUri (uri : Lsp.DocumentUri) : IO Name

Finds the module name corresponding to uri in srcSearchPath.

Equations

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

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

Converts an UTF-8-based Lean.Syntax.Range in text to an equivalent LSP UTF-16-based Lsp.Range in text.

Equations

• Lean.Syntax.Range.toLspRange text r = { start := text.utf8PosToLspPos r.start, «end» := text.utf8PosToLspPos r.stop }