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.

• 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

• Lean.Server.instInhabitedDocumentMeta

instance Lean.Server.instInhabitedDocumentMeta : Inhabited DocumentMeta

Equations

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

def Lean.Server.DocumentMeta.mkInputContext (doc : DocumentMeta) : 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 : 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.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 : 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) (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 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 : SearchPath) (uri : Lean.Lsp.DocumentUri) : IO (Option Lean.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.