structure Lapis.Server.WorkspaceEdit.AnnotatedTextEdit : Type

An optional identifier to a text edit

• range : Protocol.Types.Range
• newText : String
• annotationId : Option String

def Lapis.Server.WorkspaceEdit.instInhabitedAnnotatedTextEdit.default : AnnotatedTextEdit

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedAnnotatedTextEdit.default = { range := default, newText := default, annotationId := default }

instance Lapis.Server.WorkspaceEdit.instInhabitedAnnotatedTextEdit : Inhabited AnnotatedTextEdit

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedAnnotatedTextEdit = { default := Lapis.Server.WorkspaceEdit.instInhabitedAnnotatedTextEdit.default }

instance Lapis.Server.WorkspaceEdit.instToJsonAnnotatedTextEdit : Lean.ToJson AnnotatedTextEdit

Equations

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

instance Lapis.Server.WorkspaceEdit.instFromJsonAnnotatedTextEdit : Lean.FromJson AnnotatedTextEdit

Equations

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

structure Lapis.Server.WorkspaceEdit.CreateFileOptions : Type

Options for creating a file

• overwrite : Option Bool
• ignoreIfExists : Option Bool

instance Lapis.Server.WorkspaceEdit.instInhabitedCreateFileOptions : Inhabited CreateFileOptions

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedCreateFileOptions = { default := Lapis.Server.WorkspaceEdit.instInhabitedCreateFileOptions.default }

def Lapis.Server.WorkspaceEdit.instInhabitedCreateFileOptions.default : CreateFileOptions

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedCreateFileOptions.default = { overwrite := default, ignoreIfExists := default }

instance Lapis.Server.WorkspaceEdit.instToJsonCreateFileOptions : Lean.ToJson CreateFileOptions

Equations

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

instance Lapis.Server.WorkspaceEdit.instFromJsonCreateFileOptions : Lean.FromJson CreateFileOptions

Equations

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

structure Lapis.Server.WorkspaceEdit.RenameFileOptions : Type

Options for renaming a file

• overwrite : Option Bool
• ignoreIfExists : Option Bool

def Lapis.Server.WorkspaceEdit.instInhabitedRenameFileOptions.default : RenameFileOptions

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedRenameFileOptions.default = { overwrite := default, ignoreIfExists := default }

instance Lapis.Server.WorkspaceEdit.instInhabitedRenameFileOptions : Inhabited RenameFileOptions

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedRenameFileOptions = { default := Lapis.Server.WorkspaceEdit.instInhabitedRenameFileOptions.default }

instance Lapis.Server.WorkspaceEdit.instToJsonRenameFileOptions : Lean.ToJson RenameFileOptions

Equations

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

instance Lapis.Server.WorkspaceEdit.instFromJsonRenameFileOptions : Lean.FromJson RenameFileOptions

Equations

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

structure Lapis.Server.WorkspaceEdit.DeleteFileOptions : Type

Options for deleting a file

• recursive : Option Bool
• ignoreIfNotExists : Option Bool

instance Lapis.Server.WorkspaceEdit.instInhabitedDeleteFileOptions : Inhabited DeleteFileOptions

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedDeleteFileOptions = { default := Lapis.Server.WorkspaceEdit.instInhabitedDeleteFileOptions.default }

def Lapis.Server.WorkspaceEdit.instInhabitedDeleteFileOptions.default : DeleteFileOptions

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedDeleteFileOptions.default = { recursive := default, ignoreIfNotExists := default }

instance Lapis.Server.WorkspaceEdit.instToJsonDeleteFileOptions : Lean.ToJson DeleteFileOptions

Equations

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

instance Lapis.Server.WorkspaceEdit.instFromJsonDeleteFileOptions : Lean.FromJson DeleteFileOptions

Equations

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

structure Lapis.Server.WorkspaceEdit.CreateFile : Type

Create file operation

• uri : Protocol.Types.DocumentUri
• options : Option CreateFileOptions
• annotationId : Option String

instance Lapis.Server.WorkspaceEdit.instInhabitedCreateFile : Inhabited CreateFile

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedCreateFile = { default := Lapis.Server.WorkspaceEdit.instInhabitedCreateFile.default }

def Lapis.Server.WorkspaceEdit.instInhabitedCreateFile.default : CreateFile

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedCreateFile.default = { uri := default, options := default, annotationId := default }

instance Lapis.Server.WorkspaceEdit.instToJsonCreateFile : Lean.ToJson CreateFile

Equations

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

structure Lapis.Server.WorkspaceEdit.RenameFile : Type

Rename file operation

• oldUri : Protocol.Types.DocumentUri
• newUri : Protocol.Types.DocumentUri
• options : Option RenameFileOptions
• annotationId : Option String

instance Lapis.Server.WorkspaceEdit.instInhabitedRenameFile : Inhabited RenameFile

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedRenameFile = { default := Lapis.Server.WorkspaceEdit.instInhabitedRenameFile.default }

def Lapis.Server.WorkspaceEdit.instInhabitedRenameFile.default : RenameFile

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedRenameFile.default = { oldUri := default, newUri := default, options := default, annotationId := default }

instance Lapis.Server.WorkspaceEdit.instToJsonRenameFile : Lean.ToJson RenameFile

Equations

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

structure Lapis.Server.WorkspaceEdit.DeleteFile : Type

Delete file operation

• uri : Protocol.Types.DocumentUri
• options : Option DeleteFileOptions
• annotationId : Option String

instance Lapis.Server.WorkspaceEdit.instInhabitedDeleteFile : Inhabited DeleteFile

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedDeleteFile = { default := Lapis.Server.WorkspaceEdit.instInhabitedDeleteFile.default }

def Lapis.Server.WorkspaceEdit.instInhabitedDeleteFile.default : DeleteFile

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedDeleteFile.default = { uri := default, options := default, annotationId := default }

instance Lapis.Server.WorkspaceEdit.instToJsonDeleteFile : Lean.ToJson DeleteFile

Equations

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

structure Lapis.Server.WorkspaceEdit.TextDocumentEdit : Type

Text document edit

• textDocument : Protocol.Types.VersionedTextDocumentIdentifier
• edits : Array Protocol.Types.TextEdit

instance Lapis.Server.WorkspaceEdit.instInhabitedTextDocumentEdit : Inhabited TextDocumentEdit

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedTextDocumentEdit = { default := Lapis.Server.WorkspaceEdit.instInhabitedTextDocumentEdit.default }

def Lapis.Server.WorkspaceEdit.instInhabitedTextDocumentEdit.default : TextDocumentEdit

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedTextDocumentEdit.default = { textDocument := default, edits := default }

instance Lapis.Server.WorkspaceEdit.instToJsonTextDocumentEdit : Lean.ToJson TextDocumentEdit

Equations

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

instance Lapis.Server.WorkspaceEdit.instFromJsonTextDocumentEdit : Lean.FromJson TextDocumentEdit

Equations

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

inductive Lapis.Server.WorkspaceEdit.DocumentChange : Type

A document change can be a text edit, create, rename, or delete

• textEdit (edit : TextDocumentEdit) : DocumentChange
• createFile (create : CreateFile) : DocumentChange
• renameFile (rename : RenameFile) : DocumentChange
• deleteFile (delete : DeleteFile) : DocumentChange

def Lapis.Server.WorkspaceEdit.instInhabitedDocumentChange.default : DocumentChange

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedDocumentChange.default = Lapis.Server.WorkspaceEdit.DocumentChange.textEdit default

instance Lapis.Server.WorkspaceEdit.instInhabitedDocumentChange : Inhabited DocumentChange

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedDocumentChange = { default := Lapis.Server.WorkspaceEdit.instInhabitedDocumentChange.default }

instance Lapis.Server.WorkspaceEdit.instToJsonDocumentChange : Lean.ToJson DocumentChange

Equations

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

structure Lapis.Server.WorkspaceEdit.ChangeAnnotation : Type

Change annotation for describing edit metadata

• label : String
• needsConfirmation : Option Bool
• description : Option String

def Lapis.Server.WorkspaceEdit.instInhabitedChangeAnnotation.default : ChangeAnnotation

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedChangeAnnotation.default = { label := default, needsConfirmation := default, description := default }

instance Lapis.Server.WorkspaceEdit.instInhabitedChangeAnnotation : Inhabited ChangeAnnotation

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedChangeAnnotation = { default := Lapis.Server.WorkspaceEdit.instInhabitedChangeAnnotation.default }

instance Lapis.Server.WorkspaceEdit.instToJsonChangeAnnotation : Lean.ToJson ChangeAnnotation

Equations

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

instance Lapis.Server.WorkspaceEdit.instFromJsonChangeAnnotation : Lean.FromJson ChangeAnnotation

Equations

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

structure Lapis.Server.WorkspaceEdit.WorkspaceEdit : Type

A workspace edit represents changes to many resources

• changes : Option (Std.HashMap String (Array Protocol.Types.TextEdit))

  Map of document URI to text edits (simple format)

• documentChanges : Option (Array DocumentChange)

  Document changes (rich format with file operations)

• changeAnnotations : Option (Std.HashMap String ChangeAnnotation)

  Change annotations

instance Lapis.Server.WorkspaceEdit.instInhabitedWorkspaceEdit : Inhabited WorkspaceEdit

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedWorkspaceEdit = { default := Lapis.Server.WorkspaceEdit.instInhabitedWorkspaceEdit.default }

def Lapis.Server.WorkspaceEdit.instInhabitedWorkspaceEdit.default : WorkspaceEdit

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedWorkspaceEdit.default = { changes := default, documentChanges := default, changeAnnotations := default }

instance Lapis.Server.WorkspaceEdit.instToJsonWorkspaceEdit : Lean.ToJson WorkspaceEdit

Equations

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

structure Lapis.Server.WorkspaceEdit.ApplyWorkspaceEditParams : Type

Parameters for workspace/applyEdit request

• label : Option String
• edit : WorkspaceEdit

def Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditParams.default : ApplyWorkspaceEditParams

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditParams.default = { label := default, edit := default }

instance Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditParams : Inhabited ApplyWorkspaceEditParams

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditParams = { default := Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditParams.default }

instance Lapis.Server.WorkspaceEdit.instToJsonApplyWorkspaceEditParams : Lean.ToJson ApplyWorkspaceEditParams

Equations

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

structure Lapis.Server.WorkspaceEdit.ApplyWorkspaceEditResult : Type

Response from workspace/applyEdit

• applied : Bool
• failureReason : Option String
• failedChange : Option Nat

def Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditResult.default : ApplyWorkspaceEditResult

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditResult.default = { applied := default, failureReason := default, failedChange := default }

instance Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditResult : Inhabited ApplyWorkspaceEditResult

Equations

• Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditResult = { default := Lapis.Server.WorkspaceEdit.instInhabitedApplyWorkspaceEditResult.default }

instance Lapis.Server.WorkspaceEdit.instFromJsonApplyWorkspaceEditResult : Lean.FromJson ApplyWorkspaceEditResult

Equations

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

structure Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder : Type

Builder for constructing workspace edits

• changes : Std.HashMap String (Array Protocol.Types.TextEdit)
• documentChanges : Array DocumentChange
• annotations : Std.HashMap String ChangeAnnotation
• useDocumentChanges : Bool

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.new (useDocumentChanges : Bool := false) : WorkspaceEditBuilder

Create a new builder

Equations

• Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.new useDocumentChanges = { changes := ∅, documentChanges := #[], annotations := ∅, useDocumentChanges := useDocumentChanges }

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.addEdit (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (edit : Protocol.Types.TextEdit) : WorkspaceEditBuilder

Add a text edit to a document

Equations

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

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.addEdits (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (edits : Array Protocol.Types.TextEdit) : WorkspaceEditBuilder

Add multiple text edits to a document

Equations

• b.addEdits uri edits = Array.foldl (fun (b' : Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder) (e : Lapis.Protocol.Types.TextEdit) => b'.addEdit uri e) b edits

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.addDocumentEdit (b : WorkspaceEditBuilder) (docEdit : TextDocumentEdit) : WorkspaceEditBuilder

Add a document edit (for documentChanges mode)

Equations

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

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.createFile (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (options : Option CreateFileOptions := none) : WorkspaceEditBuilder

Add a create file operation

Equations

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

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.renameFile (b : WorkspaceEditBuilder) (oldUri newUri : Protocol.Types.DocumentUri) (options : Option RenameFileOptions := none) : WorkspaceEditBuilder

Add a rename file operation

Equations

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

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.deleteFile (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (options : Option DeleteFileOptions := none) : WorkspaceEditBuilder

Add a delete file operation

Equations

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

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.addAnnotation (b : WorkspaceEditBuilder) (id : String) (annotation : ChangeAnnotation) : WorkspaceEditBuilder

Add a change annotation

Equations

• b.addAnnotation id annotation = { changes := b.changes, documentChanges := b.documentChanges, annotations := b.annotations.insert id annotation, useDocumentChanges := b.useDocumentChanges }

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.build (b : WorkspaceEditBuilder) : WorkspaceEdit

Build the final WorkspaceEdit

Equations

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

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.replace (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (range : Protocol.Types.Range) (newText : String) : WorkspaceEditBuilder

Replace text in a range

Equations

• b.replace uri range newText = b.addEdit uri { range := range, newText := newText }

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.insert (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (pos : Protocol.Types.Position) (text : String) : WorkspaceEditBuilder

Insert text at a position

Equations

• b.insert uri pos text = b.addEdit uri { range := { start := pos, «end» := pos }, newText := text }

def Lapis.Server.WorkspaceEdit.WorkspaceEditBuilder.delete (b : WorkspaceEditBuilder) (uri : Protocol.Types.DocumentUri) (range : Protocol.Types.Range) : WorkspaceEditBuilder

Delete a range

Equations

• b.delete uri range = b.addEdit uri { range := range, newText := "" }

def Lapis.Server.WorkspaceEdit.applyEdit (outputChannel : Transport.OutputChannel) (pendingResponses : Receiver.PendingResponses) (edit : WorkspaceEdit) (label : Option String := none) : IO ApplyWorkspaceEditResult

Apply a workspace edit via the client

Equations

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

def Lapis.Server.WorkspaceEdit.applyEditOrThrow (outputChannel : Transport.OutputChannel) (pendingResponses : Receiver.PendingResponses) (edit : WorkspaceEdit) (label : Option String := none) : IO Unit

Apply a workspace edit and throw on failure

Equations

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